On this page

A scalar variational problem for a law on the line

GaussianAnalysis.probability.variationallibrary/probability/variational.v1,764 lines80 lemmas and theorems, 11 definitionssource

Imports 0 library modules and 22 external

External: HB.structures, mathcomp.classical.all_ssreflect_compat, mathcomp.algebra.algebraic_hierarchy.ssralg, mathcomp.algebra.numeric_hierarchy.ssrnum, mathcomp.algebra.interval, mathcomp.algebra.arithmetic_tactic, mathcomp.algebra.ring_tactic, mathcomp.algebra.field_tactic, mathcomp.classical.boolp, mathcomp.classical.classical_sets, mathcomp.classical.functions, mathcomp.reals.reals, mathcomp.analysis.ereal, mathcomp.analysis.topology_theory.topology, mathcomp.analysis.normedtype_theory.normedtype, mathcomp.analysis.sequences, mathcomp.analysis.measure_theory.measure, mathcomp.analysis.lebesgue_measure, mathcomp.analysis.measurable_realfun, mathcomp.analysis.numfun, mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral, mathcomp.analysis.probability_theory.probability

Imported by 1

GaussianAnalysis.probability.clip_profile

Required by 13 files of the paper proofs

For a law mu on the line with a finite second moment, the upper partial moments m(w) = E (X - w)_+ and s(w) = E (X - w)_+^2 solve the variational problem of Koehler and Sohn (arXiv 2608.27372, Lemmas 5.7 and 5.8): for c > -1 and z real, the equation w + z = c m(w) has a unique solution w, and

sup { (E (X + z) f(X))_+^2 / (E f(X)^2 + c (E f(X))^2) :
      f >= 0, E f(X)^2 < oo, E f(X) > 0 }  =  s(w) + c m(w)^2,

attained at f(x) = (x - w)_+ when the right-hand side is positive.

Main results:

upper_moment1_lipschitz: 0 <= m(w1) - m(w2) <= w2 - w1 for w1 <= w2; upper_moment1_ge: E X - w <= m(w); upper_moment1_le: m(w) <= E X^2 / (4 w) for w > 0; upper_moment1_gt0: m(w) > 0 if mu(]b, +oo[) > 0 for some b > w; upper_moment2_taylor: |s(w + h) - s(w) + 2 h m(w)| <= h^2, so s' = -2 m; upper_moment2_lipschitz: 0 <= s(a) - s(b) <= (b - a) (m(a) + m(b)) for a <= b; upper_moment2_eq0: m(w) = 0 forces s(w) = 0.
Lemma 5.7, first part, for c > -1: upper_cutoffE (w = upper_cutoff mu c z solves w + z = c m(w)), upper_cutoff_unique (it is the only solution), upper_cutoff_le (w' + z <= c m(w') if and only if w' <= w); upper_cutoff_growth: (w2 - c m(w2)) - (w1 - c m(w1)) >= min(1, 1 + c) (w2 - w1) for w1 <= w2.
upper_energy_decr: E = s + c m^2 is strictly decreasing where m > 0, E(w1) - E(w2) >= 2 min(1, 1 + c) m(w2) (w2 - w1) for w1 <= w2, hence upper_energy_lt: E(w2) < E(w1) for w1 < w2 with m(w2) > 0; upper_energy_lipschitz: |E(a) - E(b)| <= 2 (1 + |c|) m(a) (b - a), hence upper_energy_continuous; upper_energy_ge: E(w) >= (1 + c) m(w)^2.
Lemma 5.7 (upper_variational): the supremum of upper_ratio mu c z f over f in upper_admissible mu is upper_value mu c z. upper_variational_le: (E (X + z) f(X))_+^2 <= upper_value mu c z (E f(X)^2 + c (E f(X))^2) for every measurable f >= 0 with f^2 integrable; upper_variational_attained: E (X + z) p(X) = upper_value mu c z for p(x) = (x - w)_+; upper_admissible_cutoff, upper_ratio_cutoff: p is admissible and optimal when the value is positive.
upper_value_nondecr, upper_value_incr: z |-> upper_value mu c z is nondecreasing, and strictly increasing where it is positive.
Lemma 5.8: upper_cutoff_stability, upper_value_stability bound the cutoff and the value of mu by those of nu through the values of m and s at the cutoff of nu only; upper_cutoff_cvg, upper_value_cvg: if m_{mu_n} and s_{mu_n} converge to m_mu and s_mu at the cutoff of mu, the cutoffs and the values of mu_n converge to those of mu.
Symmetric laws (the scalar part of Lemma 5.9), mu invariant under x |-> -x: integrable_sym, Rintegral_sym, Rintegral_id_sym (f(-X) is integrable with f(X), E f(-X) = E f(X), E X = 0); upper_moment1_sym: m(-w) = m(w) + w; upper_moment2_sym: s(-w) + s(w) = E X^2 + w^2; upper_cutoff_dual: the cutoff of (-c/(1 + c), -z/(1 + c)) is minus that of (c, z); upper_value_dual: the two values add up to E X^2 + z^2 / (1 + c); upper_variational_sym_le: at z = 0 the bound of upper_variational_le holds without the positive part, (E X f(X))^2 <= upper_value mu c 0 (E f(X)^2 + c (E f(X))^2) (Proposition 5.10 (ii)).
The energy of a two-sided clip: clip_energy mu C t = s(-t) + s(C t), the mean squared distance from X to [t, C t] for a symmetric law (clip_energyE), and clip_value mu C, its infimum over t >= 0. clip_energy_taylor: its derivative in t is 2 (m(-t) - C m(C t)); clip_value_attained: a point t0 >= 0 where the derivative changes sign from <= 0 to >= 0 is a minimum; clip_energy_C, clip_value_nincr: nonincreasing in C, with a Lipschitz bound. taylor_nincr, taylor_ndecr: a function with a Taylor bound |F(t + h) - F(t) - h g(t)| <= K h^2 is monotone where g has a sign (a discrete integration).
Tools: Rintegral_sqr_le ((E g)^2 <= E g^2), discriminant_le (a quadratic a + 2 b t + k t^2 >= 0 for all t has b^2 <= a k), upper_form_ge0 (E f^2 + c (E f)^2 >= 0 for c > -1), integrable_of_sqr, integrable_mul_sqr, integrable_quad_bound, Rintegral_prob_cst.
Finite samples: empirical s is the law of an element of a nonempty list s drawn uniformly, a probability (the Dirac mass at 0 for the empty list), with ge0_integral_empirical, integrable_empirical, Rintegral_empirical: integrals against it are averages over s. For g : 'I_d -> R, empirical_fun g is the empirical law of its values and upper_moment_empirical_fun gives m and s as averages.
empirical_variational_le, the finite form of Lemma 5.7 for c >= 0, with weights that need not be functions of the values: for r i >= 0, (1/d) sum_i (g i + z) r i <= sqrt V sqrt ((1/d) sum_i r i^2 + c ((1/d) sum_i r i)^2), V = upper_value (empirical_fun g) c z; empirical_variational_attained: equality of (1/d) sum_i (g i + z) p i with V at p i = (g i - w)_+, w the cutoff.

Laws on the line are probabilities on measurableTypeR R, as in fourier/charfun.v. A finite second moment is the integrability of x^2.

`upper_moment mu k w`	\int[mu]_x ((x - w)_+)^k, the upper partial moment of order k at w: m(w) for k = 1, s(w) for k = 2
`upper_energy mu c w`	s(w) + c m(w)^2
`upper_cutoff mu c z`	sup {w \| w + z <= c m(w)}, the solution of w + z = c m(w) when c > -1
`upper_value mu c z`	upper_energy mu c (upper_cutoff mu c z), the value of the variational problem
`upper_admissible mu`	the measurable f >= 0 with f^2 integrable and E f > 0
`upper_ratio mu c z f`	(E (X + z) f(X))_+^2 / (E f(X)^2 + c (E f(X))^2)
`empirical s`	the average of the Dirac masses at the elements of s
`empirical_fun g`	empirical [seq g i \| i <- enum 'I_d]
`clip_energy mu C t`	s(-t) + s(C t)
`clip_value mu C`	the infimum of clip_energy mu C t over t >= 0

Main results

Results	Statement
upper_momentupper_moment1_lipschitzupper_moment1_geupper_moment1_leupper_moment1_gt0upper_moment2_taylorupper_moment2_lipschitz	For a law `mu` on the line with a finite second moment, the upper partial moments `m(w) = E (X - w)_+` and `s(w) = E (X - w)_+^2`: `m` is nonincreasing and 1-Lipschitz, `E X - w <= m(w) <= E X^2 / (4 w)` for `w > 0`, `m(w) > 0` if `mu(]b, +oo[) > 0` for some `b > w`, and `\|s(w + h) - s(w) + 2 h m(w)\| <= h^2`, so `s' = -2 m`.
upper_cutoffupper_cutoffEupper_cutoff_uniqueupper_cutoff_le	For `c > -1`, the equation `w + z = c m(w)` has exactly one solution, `upper_cutoff mu c z = sup {w \| w + z <= c m(w)}`, and the half-line `{w \| w + z <= c m(w)}` is `]-oo, upper_cutoff mu c z]` (Koehler-Sohn, Lemma 5.7).
upper_energy_decrupper_energy_ltupper_energy_lipschitzupper_energy_continuousupper_energy_ge	For `c > -1`, the energy `E = s + c m^2` satisfies `E(w1) - E(w2) >= 2 min(1, 1 + c) m(w2) (w2 - w1)` for `w1 <= w2`: it is strictly decreasing where `m > 0`; `\|E(a) - E(b)\| <= 2 (1 + \|c\|) m(a) (b - a)` for `a <= b`, so `E` is continuous; and `E(w) >= (1 + c) m(w)^2` for every `c`.
clip_energyclip_valueclip_energyEclip_energy_taylorclip_value_attainedclip_energy_Cclip_value_nincrtaylor_nincrtaylor_ndecr	For a law with a finite second moment, `clip_energy mu C t = s(-t) + s(C t)`, which for a symmetric law is the mean of `(t - X)_+^2 + (X - C t)_+^2`, the mean squared distance from `X` to `[t, C t]` when `t <= C t` (for example `C >= 1` and `t >= 0`), and its infimum `clip_value mu C` over `t >= 0`. Its derivative in `t` is `2 (m(-t) - C m(C t))` (a Taylor bound with remainder `(1 + C^2) h^2`), so a `t0 >= 0` where the derivative is `<= 0` before and `>= 0` after is a minimum. It is nonincreasing in `C`, with `0 <= clip_energy C t - clip_energy C' t <= (C' - C) t (m(C t) + m(C' t))` for `C <= C'`. The tool: a function with `\|F(t + h) - F(t) - h g(t)\| <= K h^2` for `h >= 0` is nonincreasing where `g <= 0` and nondecreasing where `g >= 0`.
upper_variationalupper_variational_leupper_variational_attained	Lemma 5.7 of Koehler and Sohn: for `c > -1` and `w` the cutoff, the supremum of `(E (X + z) f(X))_+^2 / (E f(X)^2 + c (E f(X))^2)` over measurable `f >= 0` with `E f^2 < oo` and `E f > 0` is `s(w) + c m(w)^2`, attained at `f(x) = (x - w)_+` when positive.
upper_value_nondecrupper_value_incr	The value `z \|-> s(w_z) + c m(w_z)^2` is nondecreasing, and strictly increasing where it is positive.
upper_cutoff_stabilityupper_value_stabilityupper_cutoff_cvgupper_value_cvg	Lemma 5.8 of Koehler and Sohn, quantitatively: the cutoff and the value of a law `mu` differ from those of `nu` by explicit amounts that depend only on `m_mu`, `s_mu`, `m_nu`, `s_nu` at the cutoff of `nu`; so if `m_{mu_n}` and `s_{mu_n}` converge to `m_mu` and `s_mu` at the cutoff of `mu` (no local uniform convergence needed), the cutoffs and the values converge.
upper_moment1_symupper_moment2_symupper_cutoff_dualupper_value_dualupper_variational_sym_le	For a law invariant under `x \|-> -x` with `E X^2 = v`: `m(-w) = m(w) + w`, `s(-w) + s(w) = v + w^2`, and for `c > -1`, `c' = -c / (1 + c)`, `z' = -z / (1 + c)`, the cutoff of `(c', z')` is minus that of `(c, z)` and the two values add up to `v + z^2 / (1 + c)` (the scalar part of Lemma 5.9); at `z = 0` the variational bound holds without the positive part, `(E X f(X))^2 <= value (E f(X)^2 + c (E f(X))^2)` (Proposition 5.10 (ii)).
Rintegral_sqr_lediscriminant_leintegrable_symRintegral_sym	`(E g)^2 <= E g^2`; a quadratic polynomial `a + 2 b t + k t^2` that is nonnegative for all `t`, with `k >= 0`, has `b^2 <= a k`; a law invariant under `x \|-> -x` makes `f(-X)` integrable with `f(X)` and gives `E f(-X) = E f(X)`.
empiricalempirical_setTge0_integral_empiricalintegrable_empiricalRintegral_empiricalempirical_funupper_moment_empirical_fun	The empirical law of a nonempty list `s` of reals, the average of the Dirac masses at its elements, is a probability on the line; integrals against it are averages over `s`, so the upper partial moments of the empirical law of `g_1, ..., g_d` are `(1/d) sum_i (g_i - w)_+^k`.
empirical_variational_leempirical_variational_attained	The finite form of Lemma 5.7 of Koehler and Sohn for `c >= 0`, with weights that need not be functions of the values: for `r_i >= 0`, `(1/d) sum_i (g_i + z) r_i <= sqrt V ((1/d) sum_i r_i^2 + c ((1/d) sum_i r_i)^2)^(1/2)`, `V` the value of the empirical law of the `g_i`, with equality at `r_i = (g_i - w)_+`, `w` the cutoff.

Declarations93 exported, 31 local

sectionupper_moments

Context {R : realType} (mu : probability (measurableTypeR R) R).

definition upper_moment main result source, line 123

Type

forall {R : realType}, probability (measurableTypeR R) R -> nat -> R -> R

Definition

Definition upper_moment (k : nat) (w : R) : R :=
  \int[mu]_x (Num.max ((x : R) - w) 0 ^+ k).

Main result, as the README states it

For a law mu on the line with a finite second moment, the upper partial moments m(w) = E (X - w)_+ and s(w) = E (X - w)_+^2: m is nonincreasing and 1-Lipschitz, E X - w <= m(w) <= E X^2 / (4 w) for w > 0, m(w) > 0 if mu(]b, +oo[) > 0 for some b > w, and |s(w + h) - s(w) + 2 h m(w)| <= h^2, so s' = -2 m.

Used by 55 declarations in 2 files

this file: upper_energy, upper_cutoff, upper_moment_ge0, upper_moment1_lipschitz, upper_moment1_ge, upper_moment1_le, upper_moment1_gt0, upper_moment2_taylor, upper_cutoff_growth, upper_cutoff_lipschitz, H_growth, H_lip, AE, A0, Aub, hasA, H_sup, upper_cutoffE, upper_cutoff_le, upper_cutoff_unique, upper_energy_decr, upper_moment2_eq0, Ep, Ep2, upper_variational_le, upper_moment1_cutoff_gt0, upper_value_incr, upper_moment2_lipschitz, upper_energy_lipschitz, upper_energy_continuous, upper_energy_lt, upper_energy_ge, upper_cutoff_stability, upper_value_stability, d, upper_value_cvg, upper_reflect, upper_moment1_sym, upper_moment2_sym, upper_cutoff_dual, upper_value_dual, upper_moment_empirical_fun, empirical_variational_le, clip_energy, clip_energy_taylor, clip_value_attained, clip_energy_C
GaussianAnalysis.probability.clip_profile: clip_energy_shift, upper_moment1_reflect, clip_profile_mean, clip_energy_shiftE, clip_first_order, clip_residual_profile, clip_xupperE, clip_objectiveE

definition upper_energy source, line 126

Type

forall {R : realType}, probability (measurableTypeR R) R -> R -> R -> R

Definition

Definition upper_energy (c w : R) : R :=
  upper_moment 2 w + c * upper_moment 1 w ^+ 2.

Used by 11 declarations in 1 file

this file: upper_value, upper_energy_decr, upper_variational_attained, upper_variational_le, upper_moment1_cutoff_gt0, upper_energy_lipschitz, upper_energy_continuous, upper_energy_lt, upper_energy_ge, upper_value_stability, upper_value_dual

definition upper_cutoff main result source, line 129

Type

forall {R : realType}, probability (measurableTypeR R) R -> R -> R -> R

Definition

Definition upper_cutoff (c z : R) : R :=
  sup [set w : R | w + z <= c * upper_moment 1 w].

Main result, as the README states it

For c > -1, the equation w + z = c m(w) has exactly one solution, upper_cutoff mu c z = sup {w | w + z <= c m(w)}, and the half-line {w | w + z <= c m(w)} is ]-oo, upper_cutoff mu c z] (Koehler-Sohn, Lemma 5.7).

Used by 21 declarations in 1 file

this file: upper_value, upper_cutoffE, upper_cutoff_le, upper_cutoff_unique, p, p2i, Ep, Ep2, upper_variational_attained, upper_variational_le, upper_moment1_cutoff_gt0, upper_value_incr, upper_cutoff_stability, upper_value_stability, d, upper_cutoff_cvg, upper_value_cvg, upper_cutoff_dual, upper_value_dual, empirical_variational_le, empirical_variational_attained

definition upper_value source, line 132

Type

forall {R : realType}, probability (measurableTypeR R) R -> R -> R -> R

Definition

Definition upper_value (c z : R) : R := upper_energy c (upper_cutoff c z).

Used by 16 declarations in 1 file

this file: upper_value_ge0, upper_variational_attained, upper_variational_le, upper_moment1_cutoff_gt0, upper_ratio_le, upper_admissible_cutoff, upper_ratio_cutoff, upper_variational, upper_value_nondecr, upper_value_incr, upper_value_stability, upper_value_cvg, upper_value_dual, upper_variational_sym_le, empirical_variational_le, empirical_variational_attained

definition upper_admissible source, line 134

Type

forall {R : realType}, probability (measurableTypeR R) R -> set (measurableTypeR R -> R)

Definition

Definition upper_admissible : set (measurableTypeR R -> R) :=
  [set f : measurableTypeR R -> R |
    [/\ measurable_fun [set: measurableTypeR R] f, (forall x, 0 <= f x),
    mu.-integrable [set: measurableTypeR R] (EFin \o (fun x => f x ^+ 2)) &
    0 < \int[mu]_x f x]].

Used by 8 declarations in 1 file

this file: upper_ratio_le, upper_ratio_ge0, upper_admissible_cst, upper_admissible_cutoff, upper_variational, upper_ratio_nondecr, upper_value_nondecr, upper_value_incr

definition upper_ratio source, line 140

Type

forall {R : realType},
probability (measurableTypeR R) R -> R -> R -> (measurableTypeR R -> R) -> R

Definition

Definition upper_ratio (c z : R) (f : measurableTypeR R -> R) : R :=
  Num.max (\int[mu]_x (((x : R) + z) * f x)) 0 ^+ 2 /
  (\int[mu]_x (f x ^+ 2) + c * (\int[mu]_x f x) ^+ 2).

Used by 7 declarations in 1 file

this file: upper_ratio_le, upper_ratio_ge0, upper_ratio_cutoff, upper_variational, upper_ratio_nondecr, upper_value_nondecr, upper_value_incr

sectionupper_moment_theory

Context {R : realType} (mu : probability (measurableTypeR R) R).
Hypothesis mu2 :
  mu.-integrable [set: measurableTypeR R] (EFin \o (fun x => (x : R) ^+ 2)).
Local Notation m := (upper_moment mu 1).
Local Notation s := (upper_moment mu 2).
Local Notation integrable f :=
  (mu.-integrable [set: measurableTypeR R] (EFin \o f)).

let mx section-local source, line 156

Let mx : measurable_fun [set: measurableTypeR R] (fun x => x : R).

Used by 3 declarations in 1 file

this file: upper_variational_le, upper_ratio_nondecr, upper_value_incr

lemma Rintegral_prob_cst source, line 159

forall {R : realType} (mu : probability (measurableTypeR R) R) (r : R), \int[mu]__ r = r

Statement as written in the source

Lemma Rintegral_prob_cst (r : R) : \int[mu]_x r = r.

Used by 9 declarations in 2 files

this file: upper_moment1_lipschitz, upper_moment1_ge, upper_moment2_taylor, Rintegral_sqr_le, upper_admissible_cst, upper_moment1_sym, upper_moment2_sym
GaussianAnalysis.probability.clip_profile: clip_res_sqE, clip_profile_mean

local lemma integrableZl_R not exported source, line 164

forall {R : realType} [mu : probability (measurableTypeR R) R] 
  (k : R) [f : measurableTypeR R -> R],
mu.-integrable [set: measurableTypeR R] (EFin \o f) ->
mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : measurableTypeR R => k * f x))

Statement as written in the source

Local Lemma integrableZl_R (k : R) (f : measurableTypeR R -> R) :
  integrable f -> integrable (fun x => k * f x).

Used by 13 declarations in 1 file

this file: integrable_quad_bound, upper_moment1_le, upper_moment1_gt0, upper_moment2_taylor, Rintegral_sqr_le, upper_energy_decr, upper_variational_attained, upper_variational_le, upper_ratio_nondecr, upper_value_incr, upper_moment2_lipschitz, upper_moment2_sym, upper_variational_sym_le

local lemma integrableD_R not exported source, line 171

forall {R : realType} [mu : probability (measurableTypeR R) R]
  [f g : measurableTypeR R -> R],
mu.-integrable [set: measurableTypeR R] (EFin \o f) ->
mu.-integrable [set: measurableTypeR R] (EFin \o g) ->
mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : measurableTypeR R => f x + g x))

Statement as written in the source

Local Lemma integrableD_R (f g : measurableTypeR R -> R) :
  integrable f -> integrable g -> integrable (fun x => f x + g x).

Used by 8 declarations in 1 file

this file: integrable_quad_bound, upper_moment2_taylor, integrable_of_sqr, integrable_mul_sqr, upper_variational_le, upper_ratio_nondecr, upper_value_incr, upper_moment2_lipschitz

local lemma integrableB_R not exported source, line 178

forall {R : realType} [mu : probability (measurableTypeR R) R]
  [f g : measurableTypeR R -> R],
mu.-integrable [set: measurableTypeR R] (EFin \o f) ->
mu.-integrable [set: measurableTypeR R] (EFin \o g) ->
mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : measurableTypeR R => f x - g x))

Statement as written in the source

Local Lemma integrableB_R (f g : measurableTypeR R -> R) :
  integrable f -> integrable g -> integrable (fun x => f x - g x).

Used by 7 declarations in 1 file

this file: upper_moment1_lipschitz, upper_moment1_ge, upper_moment2_taylor, Rintegral_sqr_le, upper_energy_decr, upper_moment2_lipschitz, upper_moment2_sym

local lemma integrable_norm_R not exported source, line 185

forall {R : realType} [mu : probability (measurableTypeR R) R] [f : measurableTypeR R -> R],
mu.-integrable [set: measurableTypeR R] (EFin \o f) ->
mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : measurableTypeR R => `|f x|))

Statement as written in the source

Local Lemma integrable_norm_R (f : measurableTypeR R -> R) :
  integrable f -> integrable (fun x => `|f x|).

Used by 1 declaration in 1 file

this file: upper_moment2_taylor

local lemma integrable_cst_R not exported source, line 192

forall {R : realType} (mu : probability (measurableTypeR R) R) (r : R),
mu.-integrable [set: measurableTypeR R] (EFin \o (fun=> r))

Statement as written in the source

Local Lemma integrable_cst_R (r : R) : integrable (fun _ => r).

Used by 9 declarations in 1 file

this file: integrable_quad_bound, upper_moment1_lipschitz, upper_moment1_ge, upper_moment2_taylor, integrable_of_sqr, Rintegral_sqr_le, upper_admissible_cst, upper_moment1_sym, upper_moment2_sym

lemma integrable_quad_bound source, line 195

forall {R : realType} [mu : probability (measurableTypeR R) R],
mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => (x : R) ^+ 2)) ->
forall [f : measurableTypeR R -> R] [a b : R],
measurable_fun [set: measurableTypeR R] f ->
(forall x : measurableTypeR R, `|f x| <= a + b * (x : R) ^+ 2) ->
mu.-integrable [set: measurableTypeR R] (EFin \o f)

Statement as written in the source

Lemma integrable_quad_bound (f : measurableTypeR R -> R) (a b : R) :
  measurable_fun [set: measurableTypeR R] f ->
  (forall x, `|f x| <= a + b * (x : R) ^+ 2) -> integrable f.

Used by 9 declarations in 2 files

this file: integrable_upper_pow, integrable_idR, upper_energy_decr, integrable_reflect
GaussianAnalysis.probability.clip_profile: clip_integrable_bounded, clip_integrable_id_bounded, clip_integrable_res_mul, clip_integrable_res_sq, clip_first_order

lemma measurable_upper_pow source, line 207

forall {R : realType} (w : R) (k : nat),
measurable_fun [set: measurableTypeR R]
  (fun
     x : g_sigma_algebraType
           (R.-ocitv).-measurable =>
   maxr ((x : R) - w) 0 ^+ k)

Statement as written in the source

Lemma measurable_upper_pow (w : R) k :
  measurable_fun [set: measurableTypeR R]
    (fun x => Num.max ((x : R) - w) 0 ^+ k).

Used by 3 declarations in 1 file

this file: integrable_upper_pow, upper_energy_decr, upper_moment2_eq0

lemma integrable_upper_pow source, line 215

forall {R : realType} [mu : probability (measurableTypeR R) R],
mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => (x : R) ^+ 2)) ->
forall (w : R) [k : nat],
(k <= 2)%N ->
mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => maxr ((x : R) - w) 0 ^+ k))

Statement as written in the source

Lemma integrable_upper_pow (w : R) k : (k <= 2)%N ->
  integrable (fun x => Num.max ((x : R) - w) 0 ^+ k).

Used by 19 declarations in 2 files

this file: upper_moment1_lipschitz, upper_moment1_ge, upper_moment1_le, upper_moment1_gt0, upper_moment2_taylor, upper_energy_decr, upper_moment2_eq0, p2i, upper_moment2_lipschitz, upper_energy_ge, upper_reflect, upper_moment1_sym, upper_moment2_sym, clip_energyE
GaussianAnalysis.probability.clip_profile: upper_moment1_reflect, integrable_upper1, clip_energy_shiftE, clip_xupper_integrable, clip_xupperE

lemma integrable_idR source, line 231

forall {R : realType} [mu : probability (measurableTypeR R) R],
mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => (x : R) ^+ 2)) ->
mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => x : R))

Statement as written in the source

Lemma integrable_idR : integrable (fun x => x : R).

Used by 6 declarations in 2 files

this file: upper_moment1_ge, Rintegral_id_sym, upper_moment1_sym, upper_moment2_sym
GaussianAnalysis.probability.clip_profile: clip_res_sqE, clip_objectiveE

lemma upper_moment_ge0 source, line 238

forall {R : realType} (mu : probability (measurableTypeR R) R) (k : nat) (w : R),
0 <= upper_moment mu k w

Statement as written in the source

Lemma upper_moment_ge0 k w : 0 <= upper_moment mu k w.

Used by 7 declarations in 2 files

this file: upper_energy_decr, upper_moment1_cutoff_gt0, upper_energy_lipschitz, upper_energy_continuous, upper_value_stability, clip_energy_ge0
GaussianAnalysis.probability.clip_profile: clip_energy_shift_ge0

Pointwise facts about the positive part.

lemma upper_part_diff source, line 245

forall {R : realType} (x : R) [w1 w2 : R],
w1 <= w2 -> 0 <= maxr (x - w1) 0 - maxr (x - w2) 0 <= w2 - w1

Statement as written in the source

Lemma upper_part_diff (x w1 w2 : R) : w1 <= w2 ->
  0 <= Num.max (x - w1) 0 - Num.max (x - w2) 0 <= w2 - w1.

Used by 3 declarations in 1 file

this file: upper_moment1_lipschitz, upper_energy_decr, upper_moment2_lipschitz

lemma upper_part_sqr_taylor source, line 252

forall {R : realType} (x w h : R),
`|maxr (x - (w + h)) 0 ^+ 2 - maxr (x - w) 0 ^+ 2 + 2 * h * maxr (x - w) 0| <= h ^+ 2

Statement as written in the source

Lemma upper_part_sqr_taylor (x w h : R) :
  `|Num.max (x - (w + h)) 0 ^+ 2 - Num.max (x - w) 0 ^+ 2
    + 2 * h * Num.max (x - w) 0| <= h ^+ 2.

Used by 1 declaration in 1 file

this file: upper_moment2_taylor

Regularity of m and s.

lemma upper_moment1_lipschitz main result source, line 271

forall {R : realType} [mu : probability (measurableTypeR R) R],
mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => (x : R) ^+ 2)) ->
forall [w1 w2 : R], w1 <= w2 -> 0 <= upper_moment mu 1 w1 - upper_moment mu 1 w2 <= w2 - w1

Main result

Stated in the README together with upper_moment.

Statement as written in the source

Lemma upper_moment1_lipschitz w1 w2 : w1 <= w2 ->
  0 <= m w1 - m w2 <= w2 - w1.

Used by 6 declarations in 1 file

this file: upper_cutoff_growth, upper_cutoff_lipschitz, upper_energy_decr, upper_energy_lipschitz, upper_energy_continuous, upper_value_stability

lemma upper_moment1_ge main result source, line 284

forall {R : realType} [mu : probability (measurableTypeR R) R],
mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => (x : R) ^+ 2)) ->
forall w : R, \int[mu]_x (x : R) - w <= upper_moment mu 1 w

Main result

Stated in the README together with upper_moment.

Statement as written in the source

Lemma upper_moment1_ge w : \int[mu]_x (x : R) - w <= m w.

lemma upper_moment1_le main result source, line 295

forall {R : realType} [mu : probability (measurableTypeR R) R],
mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => (x : R) ^+ 2)) ->
forall [w : join_Num_POrderNmodule_between_Algebra_BaseAddUMagma_and_Order_Preorder R],
0 < w -> upper_moment mu 1 w <= \int[mu]_x (x : R) ^+ 2 / (4 * w)

Main result

Stated in the README together with upper_moment.

Statement as written in the source

Lemma upper_moment1_le w : 0 < w ->
  m w <= \int[mu]_x ((x : R) ^+ 2) / (4 * w).

lemma upper_moment1_gt0 main result source, line 308

forall {R : realType} [mu : probability (measurableTypeR R) R],
mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => (x : R) ^+ 2)) ->
forall [w b : R], w < b -> (0%R < mu `]b, +oo[%classic)%E -> 0 < upper_moment mu 1 w

Main result

Stated in the README together with upper_moment.

Statement as written in the source

Lemma upper_moment1_gt0 (w b : R) : w < b ->
  (0 < mu `]b, +oo[%classic)%E -> 0 < m w.

lemma upper_moment2_taylor main result source, line 330

forall {R : realType} [mu : probability (measurableTypeR R) R],
mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => (x : R) ^+ 2)) ->
forall w h : R,
`|upper_moment mu 2 (w + h) - upper_moment mu 2 w + 2 * h * upper_moment mu 1 w| <= h ^+ 2

Main result

Stated in the README together with upper_moment.

Statement as written in the source

Lemma upper_moment2_taylor w h :
  `|s (w + h) - s w + 2 * h * m w| <= h ^+ 2.

Used by 1 declaration in 1 file

this file: clip_energy_taylor

The cutoff: the solution of w + z = c m(w).

lemma upper_cutoff_growth source, line 352

forall {R : realType} [mu : probability (measurableTypeR R) R],
mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => (x : R) ^+ 2)) ->
forall [c : join_Num_POrderZmodule_between_Algebra_BaseZmodule_and_Order_Preorder R]
  [w1
   w2 : join_Num_POrderNmodule_between_Algebra_BaseAddMagma_and_Order_Preorder
          (join_Num_POrderZmodule_between_Algebra_BaseZmodule_and_Num_POrderNmodule R)],
-1 < c ->
w1 <= w2 ->
minr 1 (1 + c) * (w2 - w1) <=
w2 - c * upper_moment mu 1 w2 - (w1 - c * upper_moment mu 1 w1)

Statement as written in the source

Lemma upper_cutoff_growth c w1 w2 : -1 < c -> w1 <= w2 ->
  Num.min 1 (1 + c) * (w2 - w1) <= (w2 - c * m w2) - (w1 - c * m w1).

Used by 3 declarations in 1 file

this file: H_growth, upper_energy_decr, upper_cutoff_stability

lemma upper_cutoff_lipschitz source, line 364

forall {R : realType} [mu : probability (measurableTypeR R) R],
mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => (x : R) ^+ 2)) ->
forall (c : R)
  [w1 w2 : join_Num_POrderNmodule_between_Algebra_BaseAddMagma_and_Order_Preorder R],
w1 <= w2 ->
w2 - c * upper_moment mu 1 w2 - (w1 - c * upper_moment mu 1 w1) <= (1 + `|c|) * (w2 - w1)

Statement as written in the source

Lemma upper_cutoff_lipschitz c w1 w2 : w1 <= w2 ->
  (w2 - c * m w2) - (w1 - c * m w1) <= (1 + `|c|) * (w2 - w1).

Used by 1 declaration in 1 file

this file: H_lip

sectioncutoff

Variables (c z : R).
Hypothesis c1 : -1 < c.
Local Notation H w := (w + z - c * m w).
Local Notation A := [set w : R | w + z <= c * m w].
Local Notation delta := (Num.min 1 (1 + c)).
Local Notation L := (1 + `|c|).

let delta0 section-local source, line 385

Let delta0 : 0 < delta.

Used by 5 declarations in 1 file

this file: A0, Aub, H_sup, upper_cutoff_le, upper_cutoff_unique

let L0 section-local source, line 388

Let L0 : 0 < L.

Used by 1 declaration in 1 file

this file: H_sup

let H_growth section-local source, line 391

Let H_growth w1 w2 : w1 <= w2 -> delta * (w2 - w1) <= H w2 - H w1.

Used by 4 declarations in 1 file

this file: A0, Aub, upper_cutoff_le, upper_cutoff_unique

let H_lip section-local source, line 396

Let H_lip w1 w2 : w1 <= w2 -> H w2 - H w1 <= L * (w2 - w1).

Used by 1 declaration in 1 file

this file: H_sup

let AE section-local source, line 401

Let AE w : A w <-> H w <= 0.

Used by 4 declarations in 1 file

this file: A0, Aub, H_sup, upper_cutoff_le

let A0 section-local source, line 404

Let A0 : A !=set0.

Used by 2 declarations in 1 file

this file: hasA, H_sup

let Aub section-local source, line 415

Let Aub : ubound A (`|H 0| / delta).

Used by 1 declaration in 1 file

this file: hasA

let hasA section-local source, line 425

Let hasA : has_sup A.

Used by 2 declarations in 1 file

this file: H_sup, upper_cutoff_le

let H_sup section-local source, line 428

Let H_sup : H (sup A) = 0.

Used by 3 declarations in 1 file

this file: upper_cutoffE, upper_cutoff_le, upper_cutoff_unique

lemma upper_cutoffE main result source, line 454

forall {R : realType} [mu : probability (measurableTypeR R) R],
mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => (x : R) ^+ 2)) ->
forall [c : R] (z : R),
-1 < c -> upper_cutoff mu c z + z = c * upper_moment mu 1 (upper_cutoff mu c z)

Main result

Stated in the README together with upper_cutoff.

Statement as written in the source

Lemma upper_cutoffE : upper_cutoff mu c z + z = c * m (upper_cutoff mu c z).

Used by 6 declarations in 1 file

this file: upper_variational_attained, upper_variational_le, upper_cutoff_stability, upper_cutoff_dual, upper_value_dual, empirical_variational_le

lemma upper_cutoff_le main result source, line 457

forall {R : realType} [mu : probability (measurableTypeR R) R],
mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => (x : R) ^+ 2)) ->
forall [c : R] (z : R),
-1 < c -> forall w : R, w + z <= c * upper_moment mu 1 w <-> w <= upper_cutoff mu c z

Main result

Stated in the README together with upper_cutoff.

Statement as written in the source

Lemma upper_cutoff_le w : w + z <= c * m w <-> w <= upper_cutoff mu c z.

Used by 1 declaration in 1 file

this file: upper_cutoff_unique

lemma upper_cutoff_unique main result source, line 467

forall {R : realType} [mu : probability (measurableTypeR R) R],
mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => (x : R) ^+ 2)) ->
forall [c z : R],
-1 < c -> forall [w : R], w + z = c * upper_moment mu 1 w -> w = upper_cutoff mu c z

Main result

Stated in the README together with upper_cutoff.

Statement as written in the source

Lemma upper_cutoff_unique w : w + z = c * m w -> w = upper_cutoff mu c z.

Used by 1 declaration in 1 file

this file: upper_cutoff_dual

Squares, products and Jensen's inequality.

lemma integrable_of_sqr source, line 482

forall {R : realType} [mu : probability (measurableTypeR R) R] [f : measurableTypeR R -> R],
measurable_fun [set: measurableTypeR R] f ->
mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : measurableTypeR R => f x ^+ 2)) ->
mu.-integrable [set: measurableTypeR R] (EFin \o f)

Statement as written in the source

Lemma integrable_of_sqr (f : measurableTypeR R -> R) :
  measurable_fun [set: measurableTypeR R] f ->
  integrable (fun x => f x ^+ 2) -> integrable f.

Used by 7 declarations in 1 file

this file: pi, upper_variational_le, upper_ratio_le, upper_ratio_ge0, upper_ratio_nondecr, upper_value_incr, upper_variational_sym_le

lemma integrable_mul_sqr source, line 495

forall {R : realType} [mu : probability (measurableTypeR R) R]
  [f g : measurableTypeR R -> R],
measurable_fun [set: measurableTypeR R] f ->
measurable_fun [set: measurableTypeR R] g ->
mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : measurableTypeR R => f x ^+ 2)) ->
mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : measurableTypeR R => g x ^+ 2)) ->
mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : measurableTypeR R => f x * g x))

Statement as written in the source

Lemma integrable_mul_sqr (f g : measurableTypeR R -> R) :
  measurable_fun [set: measurableTypeR R] f ->
  measurable_fun [set: measurableTypeR R] g ->
  integrable (fun x => f x ^+ 2) -> integrable (fun x => g x ^+ 2) ->
  integrable (fun x => f x * g x).

Used by 4 declarations in 1 file

this file: upper_variational_le, upper_ratio_nondecr, upper_value_incr, upper_variational_sym_le

lemma Rintegral_sqr_le main result source, line 512

forall {R : realType} [mu : probability (measurableTypeR R) R] [g : measurableTypeR R -> R],
mu.-integrable [set: measurableTypeR R] (EFin \o g) ->
mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : measurableTypeR R => g x ^+ 2)) ->
(\int[mu]_x g x) ^+ 2 <= \int[mu]_x g x ^+ 2

Main result, as the README states it

(E g)^2 <= E g^2; a quadratic polynomial a + 2 b t + k t^2 that is nonnegative for all t, with k >= 0, has b^2 <= a k; a law invariant under x |-> -x makes f(-X) integrable with f(X) and gives E f(-X) = E f(X).

Statement as written in the source

Lemma Rintegral_sqr_le (g : measurableTypeR R -> R) :
  integrable g -> integrable (fun x => g x ^+ 2) ->
  (\int[mu]_x g x) ^+ 2 <= \int[mu]_x (g x ^+ 2).

Used by 6 declarations in 2 files

this file: upper_energy_decr, upper_form_ge0, upper_ratio_le, upper_ratio_nondecr, upper_energy_ge
GaussianAnalysis.probability.clip_profile: clip_dual_window

The energy s + c m^2 decreases.

lemma upper_part_sqr_diff source, line 532

forall {R : realType} (x : R) [w1 w2 : R],
w1 <= w2 ->
maxr (x - w1) 0 ^+ 2 - maxr (x - w2) 0 ^+ 2 =
2 * (w2 - w1) * maxr (x - w2) 0 + (maxr (x - w1) 0 - maxr (x - w2) 0) ^+ 2

Statement as written in the source

Lemma upper_part_sqr_diff (x w1 w2 : R) : w1 <= w2 ->
  Num.max (x - w1) 0 ^+ 2 - Num.max (x - w2) 0 ^+ 2 =
  2 * (w2 - w1) * Num.max (x - w2) 0
  + (Num.max (x - w1) 0 - Num.max (x - w2) 0) ^+ 2.

Used by 1 declaration in 1 file

this file: upper_energy_decr

lemma upper_energy_decr main result source, line 544

forall {R : realType} [mu : probability (measurableTypeR R) R],
mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => (x : R) ^+ 2)) ->
forall [c : join_Num_POrderZmodule_between_Algebra_BaseZmodule_and_Order_Preorder R]
  [w1 w2 : R],
-1 < c ->
w1 <= w2 ->
2 * minr 1 (1 + c) * upper_moment mu 1 w2 * (w2 - w1) <=
upper_energy mu c w1 - upper_energy mu c w2

Main result, as the README states it

For c > -1, the energy E = s + c m^2 satisfies E(w1) - E(w2) >= 2 min(1, 1 + c) m(w2) (w2 - w1) for w1 <= w2: it is strictly decreasing where m > 0; |E(a) - E(b)| <= 2 (1 + |c|) m(a) (b - a) for a <= b, so E is continuous; and E(w) >= (1 + c) m(w)^2 for every c.

Statement as written in the source

Lemma upper_energy_decr c w1 w2 : -1 < c -> w1 <= w2 ->
  2 * Num.min 1 (1 + c) * m w2 * (w2 - w1) <=
  upper_energy mu c w1 - upper_energy mu c w2.

Used by 1 declaration in 1 file

this file: upper_energy_lt

Cauchy-Schwarz through the discriminant.

lemma discriminant_le main result source, line 596

forall {R : realType} [a b k : R],
0 <= k -> (forall t : R, 0 <= a + 2 * b * t + k * t ^+ 2) -> b ^+ 2 <= a * k

Main result

Stated in the README together with Rintegral_sqr_le.

Statement as written in the source

Lemma discriminant_le (a b k : R) : 0 <= k ->
  (forall t, 0 <= a + 2 * b * t + k * t ^+ 2) -> b ^+ 2 <= a * k.

Used by 3 declarations in 2 files

this file: upper_variational_le, empirical_variational_le
GaussianAnalysis.probability.clip_profile: clip_dual_window

lemma upper_form_ge0 source, line 612

forall {R : realType} [mu : probability (measurableTypeR R) R]
  [c : join_Num_POrderZmodule_between_Algebra_BaseZmodule_and_Order_Preorder R]
  [f : measurableTypeR R -> R],
-1 < c ->
mu.-integrable [set: measurableTypeR R] (EFin \o f) ->
mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : measurableTypeR R => f x ^+ 2)) ->
0 <= \int[mu]_x f x ^+ 2 + c * (\int[mu]_x f x) ^+ 2

Statement as written in the source

Lemma upper_form_ge0 c (f : measurableTypeR R -> R) : -1 < c ->
  integrable f -> integrable (fun x => f x ^+ 2) ->
  0 <= \int[mu]_x (f x ^+ 2) + c * (\int[mu]_x f x) ^+ 2.

Used by 4 declarations in 2 files

this file: upper_value_ge0, upper_variational_le, upper_ratio_ge0
GaussianAnalysis.probability.clip_profile: clip_optimal

lemma upper_moment2_eq0 source, line 621

forall {R : realType} [mu : probability (measurableTypeR R) R],
mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => (x : R) ^+ 2)) ->
forall [w : R], upper_moment mu 1 w = 0 -> upper_moment mu 2 w = 0

Statement as written in the source

Lemma upper_moment2_eq0 w : m w = 0 -> s w = 0.

Used by 1 declaration in 1 file

this file: upper_moment1_cutoff_gt0

sectionvariational

Variables (c z : R).
Hypothesis c1 : -1 < c.
Local Notation w := (upper_cutoff mu c z).

let p section-local source, line 648

Let p (x : measurableTypeR R) := Num.max ((x : R) - w) 0.

Used by 11 declarations in 1 file

this file: p_ge0, mp, p2i, pi, Ep, Ep2, upper_variational_attained, upper_variational_le, upper_admissible_cutoff, upper_ratio_cutoff, upper_variational

let p_ge0 section-local source, line 650

Let p_ge0 x : 0 <= p x.

let mp section-local source, line 653

Let mp : measurable_fun [set: measurableTypeR R] p.

Used by 1 declaration in 1 file

this file: upper_variational_le

let p2i section-local source, line 659

Let p2i : integrable (fun x => p x ^+ 2).

Used by 2 declarations in 1 file

this file: upper_value_ge0, upper_variational_le

let pi section-local source, line 662

Let pi : integrable p.

Used by 1 declaration in 1 file

this file: upper_value_ge0

let Ep section-local source, line 665

Let Ep : \int[mu]_x p x = m w.

Used by 5 declarations in 1 file

this file: upper_value_ge0, upper_variational_attained, upper_variational_le, upper_admissible_cutoff, upper_ratio_cutoff

let Ep2 section-local source, line 668

Let Ep2 : \int[mu]_x (p x ^+ 2) = s w.

Used by 4 declarations in 1 file

this file: upper_value_ge0, upper_variational_attained, upper_variational_le, upper_ratio_cutoff

lemma upper_value_ge0 source, line 671

forall {R : realType} [mu : probability (measurableTypeR R) R],
mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => (x : R) ^+ 2)) ->
forall [c : R] (z : R), -1 < c -> 0 <= upper_value mu c z

Statement as written in the source

Lemma upper_value_ge0 : 0 <= upper_value mu c z.

Used by 2 declarations in 1 file

this file: upper_variational_le, upper_variational

lemma upper_variational_attained main result source, line 676

forall {R : realType} [mu : probability (measurableTypeR R) R],
mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => (x : R) ^+ 2)) ->
forall [c : R] (z : R),
-1 < c ->
\int[mu]_x
   (((x : R) + z) *
    (fun x0 : measurableTypeR R => maxr ((x0 : R) - upper_cutoff mu c z) 0) x) =
upper_value mu c z

Main result

Stated in the README together with upper_variational.

Statement as written in the source

Lemma upper_variational_attained :
  \int[mu]_x (((x : R) + z) * p x) = upper_value mu c z.

Used by 3 declarations in 1 file

this file: upper_ratio_cutoff, upper_value_incr, empirical_variational_attained

lemma upper_variational_le main result source, line 689

forall {R : realType} [mu : probability (measurableTypeR R) R],
mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => (x : R) ^+ 2)) ->
forall [c : R] (z : R),
-1 < c ->
forall [f : measurableTypeR R -> R],
measurable_fun [set: measurableTypeR R] f ->
(forall x : measurableTypeR R, 0 <= f x) ->
mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : measurableTypeR R => f x ^+ 2)) ->
maxr (\int[mu]_x (((x : R) + z) * f x)) 0 ^+ 2 <=
upper_value mu c z * (\int[mu]_x f x ^+ 2 + c * (\int[mu]_x f x) ^+ 2)

Main result

Stated in the README together with upper_variational.

Statement as written in the source

Lemma upper_variational_le (f : measurableTypeR R -> R) :
  measurable_fun [set: measurableTypeR R] f -> (forall x, 0 <= f x) ->
  integrable (fun x => f x ^+ 2) ->
  Num.max (\int[mu]_x (((x : R) + z) * f x)) 0 ^+ 2 <=
  upper_value mu c z * (\int[mu]_x (f x ^+ 2) + c * (\int[mu]_x f x) ^+ 2).

Used by 2 declarations in 1 file

this file: upper_ratio_le, upper_variational_sym_le

lemma upper_moment1_cutoff_gt0 source, line 748

forall {R : realType} [mu : probability (measurableTypeR R) R],
mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => (x : R) ^+ 2)) ->
forall [c z : R], 0 < upper_value mu c z -> 0 < upper_moment mu 1 (upper_cutoff mu c z)

Statement as written in the source

Lemma upper_moment1_cutoff_gt0 : 0 < upper_value mu c z -> 0 < m w.

Used by 2 declarations in 1 file

this file: upper_admissible_cutoff, upper_value_incr

lemma upper_ratio_le source, line 756

forall {R : realType} [mu : probability (measurableTypeR R) R],
mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => (x : R) ^+ 2)) ->
forall [c : R] (z : R),
-1 < c ->
forall [f : measurableTypeR R -> R],
upper_admissible mu f -> upper_ratio mu c z f <= upper_value mu c z

Statement as written in the source

Lemma upper_ratio_le f : upper_admissible mu f ->
  upper_ratio mu c z f <= upper_value mu c z.

Used by 3 declarations in 1 file

this file: upper_variational, upper_value_nondecr, upper_value_incr

lemma upper_ratio_ge0 source, line 767

forall {R : realType} [mu : probability (measurableTypeR R) R] [c : R] (z : R),
-1 < c ->
forall [f : measurableTypeR R -> R], upper_admissible mu f -> 0 <= upper_ratio mu c z f

Statement as written in the source

Lemma upper_ratio_ge0 f : upper_admissible mu f -> 0 <= upper_ratio mu c z f.

Used by 1 declaration in 1 file

this file: upper_variational

lemma upper_admissible_cst source, line 774

forall {R : realType} (mu : probability (measurableTypeR R) R),
upper_admissible mu (fun=> 1)

Statement as written in the source

Lemma upper_admissible_cst : upper_admissible mu (fun _ => 1).

Used by 2 declarations in 1 file

this file: upper_variational, upper_value_nondecr

lemma upper_admissible_cutoff source, line 781

forall {R : realType} [mu : probability (measurableTypeR R) R],
mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => (x : R) ^+ 2)) ->
forall [c z : R],
0 < upper_value mu c z ->
upper_admissible mu (fun x : measurableTypeR R => maxr ((x : R) - upper_cutoff mu c z) 0)

Statement as written in the source

Lemma upper_admissible_cutoff : 0 < upper_value mu c z -> upper_admissible mu p.

Used by 2 declarations in 1 file

this file: upper_variational, upper_value_incr

lemma upper_ratio_cutoff source, line 786

forall {R : realType} [mu : probability (measurableTypeR R) R],
mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => (x : R) ^+ 2)) ->
forall [c z : R],
-1 < c ->
0 < upper_value mu c z ->
upper_ratio mu c z (fun x : measurableTypeR R => maxr ((x : R) - upper_cutoff mu c z) 0) =
upper_value mu c z

Statement as written in the source

Lemma upper_ratio_cutoff : 0 < upper_value mu c z ->
  upper_ratio mu c z p = upper_value mu c z.

Used by 1 declaration in 1 file

this file: upper_variational

lemma upper_variational main result source, line 796

forall {R : realType} [mu : probability (measurableTypeR R) R],
mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => (x : R) ^+ 2)) ->
forall [c : R] (z : R),
-1 < c -> sup [set upper_ratio mu c z f | f in upper_admissible mu] = upper_value mu c z

Main result, as the README states it

Lemma 5.7 of Koehler and Sohn: for c > -1 and w the cutoff, the supremum of (E (X + z) f(X))_+^2 / (E f(X)^2 + c (E f(X))^2) over measurable f >= 0 with E f^2 < oo and E f > 0 is s(w) + c m(w)^2, attained at f(x) = (x - w)_+ when positive.

Statement as written in the source

Lemma upper_variational :
  sup [set upper_ratio mu c z f | f in upper_admissible mu] =
  upper_value mu c z.

Used by 1 declaration in 1 file

this file: upper_value_nondecr

lemma upper_ratio_nondecr source, line 817

forall {R : realType} [mu : probability (measurableTypeR R) R],
mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => (x : R) ^+ 2)) ->
forall [c z : R],
-1 < c ->
forall [z' : R] [f : measurableTypeR R -> R],
z <= z' -> upper_admissible mu f -> upper_ratio mu c z f <= upper_ratio mu c z' f

Statement as written in the source

Lemma upper_ratio_nondecr z' f : z <= z' -> upper_admissible mu f ->
  upper_ratio mu c z f <= upper_ratio mu c z' f.

Used by 1 declaration in 1 file

this file: upper_value_nondecr

lemma upper_value_nondecr main result source, line 843

forall {R : realType} [mu : probability (measurableTypeR R) R],
mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => (x : R) ^+ 2)) ->
forall [c : join_Num_POrderZmodule_between_Algebra_BaseZmodule_and_Order_Preorder R]
  [z z' : R],
-1 < c -> z <= z' -> upper_value mu c z <= upper_value mu c z'

Main result, as the README states it

The value z |-> s(w_z) + c m(w_z)^2 is nondecreasing, and strictly increasing where it is positive.

Statement as written in the source

Lemma upper_value_nondecr c z z' : -1 < c -> z <= z' ->
  upper_value mu c z <= upper_value mu c z'.

lemma upper_value_incr main result source, line 857

forall {R : realType} [mu : probability (measurableTypeR R) R],
mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => (x : R) ^+ 2)) ->
forall [c : join_Num_POrderZmodule_between_Algebra_BaseZmodule_and_Order_Preorder R]
  [z z' : R],
-1 < c -> z < z' -> 0 < upper_value mu c z -> upper_value mu c z < upper_value mu c z'

Main result

Stated in the README together with upper_value_nondecr.

Statement as written in the source

Lemma upper_value_incr c z z' : -1 < c -> z < z' -> 0 < upper_value mu c z ->
  upper_value mu c z < upper_value mu c z'.

lemma upper_moment2_lipschitz main result source, line 886

forall {R : realType} [mu : probability (measurableTypeR R) R],
mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => (x : R) ^+ 2)) ->
forall [a b : R],
a <= b ->
0 <= upper_moment mu 2 a - upper_moment mu 2 b <=
(b - a) * (upper_moment mu 1 a + upper_moment mu 1 b)

Main result

Stated in the README together with upper_moment.

Statement as written in the source

Lemma upper_moment2_lipschitz a b : a <= b ->
  0 <= s a - s b <= (b - a) * (m a + m b).

Used by 2 declarations in 1 file

this file: upper_energy_lipschitz, clip_energy_C

lemma upper_energy_lipschitz main result source, line 907

forall {R : realType} [mu : probability (measurableTypeR R) R],
mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => (x : R) ^+ 2)) ->
forall (c : R) [a b : R],
a <= b ->
`|upper_energy mu c a - upper_energy mu c b| <=
2 * (1 + `|c|) * upper_moment mu 1 a * (b - a)

Main result

Stated in the README together with upper_energy_decr.

Statement as written in the source

Lemma upper_energy_lipschitz c a b : a <= b ->
  `|upper_energy mu c a - upper_energy mu c b| <=
  2 * (1 + `|c|) * m a * (b - a).

Used by 2 declarations in 1 file

this file: upper_energy_continuous, upper_value_stability

lemma upper_energy_continuous main result source, line 927

forall {R : realType} [mu : probability (measurableTypeR R) R],
mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => (x : R) ^+ 2)) ->
forall [c : R], continuous (upper_energy mu c)

Main result

Stated in the README together with upper_energy_decr.

Statement as written in the source

Lemma upper_energy_continuous c : continuous (upper_energy mu c).

lemma upper_energy_lt main result source, line 960

forall {R : realType} [mu : probability (measurableTypeR R) R],
mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => (x : R) ^+ 2)) ->
forall [c : join_Num_POrderZmodule_between_Algebra_BaseZmodule_and_Order_Preorder R]
  [w1 w2 : R],
-1 < c ->
w1 < w2 -> 0 < upper_moment mu 1 w2 -> upper_energy mu c w2 < upper_energy mu c w1

Main result

Stated in the README together with upper_energy_decr.

Statement as written in the source

Lemma upper_energy_lt c w1 w2 : -1 < c -> w1 < w2 -> 0 < m w2 ->
  upper_energy mu c w2 < upper_energy mu c w1.

lemma upper_energy_ge main result source, line 969

forall {R : realType} [mu : probability (measurableTypeR R) R],
mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => (x : R) ^+ 2)) ->
forall c w : R, (1 + c) * upper_moment mu 1 w ^+ 2 <= upper_energy mu c w

Main result

Stated in the README together with upper_energy_decr.

Statement as written in the source

Lemma upper_energy_ge c w : (1 + c) * m w ^+ 2 <= upper_energy mu c w.

sectionstability

Context {R : realType} (mu nu : probability (measurableTypeR R) R).
Hypothesis mu2 :
  mu.-integrable [set: measurableTypeR R] (EFin \o (fun x => (x : R) ^+ 2)).
Hypothesis nu2 :
  nu.-integrable [set: measurableTypeR R] (EFin \o (fun x => (x : R) ^+ 2)).
Variables (c z : R).
Hypothesis c1 : -1 < c.
Local Notation w2 := (upper_cutoff nu c z).
Local Notation D := (`|upper_moment mu 1 w2 - upper_moment nu 1 w2|).
Local Notation delta := (`|c| / Num.min 1 (1 + c) * D).

lemma upper_cutoff_stability main result source, line 997

forall {R : realType} [mu nu : probability (measurableTypeR R) R],
mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => (x : R) ^+ 2)) ->
nu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => (x : R) ^+ 2)) ->
forall [c : R] (z : R),
-1 < c ->
`|upper_cutoff mu c z - upper_cutoff nu c z| <=
`|c| / minr 1 (1 + c) *
`|upper_moment mu 1 (upper_cutoff nu c z) - upper_moment nu 1 (upper_cutoff nu c z)|

Main result, as the README states it

Lemma 5.8 of Koehler and Sohn, quantitatively: the cutoff and the value of a law mu differ from those of nu by explicit amounts that depend only on m_mu, s_mu, m_nu, s_nu at the cutoff of nu; so if m_{mu_n} and s_{mu_n} converge to m_mu and s_mu at the cutoff of mu (no local uniform convergence needed), the cutoffs and the values converge.

Statement as written in the source

Lemma upper_cutoff_stability : `|upper_cutoff mu c z - w2| <= delta.

Used by 2 declarations in 1 file

this file: upper_value_stability, upper_cutoff_cvg

lemma upper_value_stability main result source, line 1021

forall {R : realType} [mu nu : probability (measurableTypeR R) R],
mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => (x : R) ^+ 2)) ->
nu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => (x : R) ^+ 2)) ->
forall [c : R] (z : R),
-1 < c ->
`|upper_value mu c z - upper_value nu c z| <=
`|upper_moment mu 2 (upper_cutoff nu c z) - upper_moment nu 2 (upper_cutoff nu c z)| +
`|c| *
`|upper_moment mu 1 (upper_cutoff nu c z) ^+ 2 -
  upper_moment nu 1 (upper_cutoff nu c z) ^+ 2| +
2 * (1 + `|c|) *
(upper_moment mu 1 (upper_cutoff nu c z) +
 `|c| / minr 1 (1 + c) *
 `|upper_moment mu 1 (upper_cutoff nu c z) - upper_moment nu 1 (upper_cutoff nu c z)|) *
(`|c| / minr 1 (1 + c) *
 `|upper_moment mu 1 (upper_cutoff nu c z) - upper_moment nu 1 (upper_cutoff nu c z)|)

Main result

Stated in the README together with upper_cutoff_stability.

Statement as written in the source

Lemma upper_value_stability :
  `|upper_value mu c z - upper_value nu c z| <=
  `|upper_moment mu 2 w2 - upper_moment nu 2 w2|
  + `|c| * `|upper_moment mu 1 w2 ^+ 2 - upper_moment nu 1 w2 ^+ 2|
  + 2 * (1 + `|c|) * (upper_moment mu 1 w2 + delta) * delta.

Used by 1 declaration in 1 file

this file: upper_value_cvg

sectionstability_cvg

Context {R : realType} (mu_ : nat -> probability (measurableTypeR R) R)
  (mu : probability (measurableTypeR R) R).
Hypothesis mu_2 : forall n, (mu_ n).-integrable [set: measurableTypeR R]
  (EFin \o (fun x => (x : R) ^+ 2)).
Hypothesis mu2 :
  mu.-integrable [set: measurableTypeR R] (EFin \o (fun x => (x : R) ^+ 2)).
Variables (c z : R).
Hypothesis c1 : -1 < c.
Local Notation w := (upper_cutoff mu c z).
Hypothesis m_cvg :
  upper_moment (mu_ n) 1 w @[n --> \oo] --> upper_moment mu 1 w.
Hypothesis s_cvg :
  upper_moment (mu_ n) 2 w @[n --> \oo] --> upper_moment mu 2 w.

let K section-local source, line 1092

Let K := `|c| / Num.min 1 (1 + c).

Used by 3 declarations in 1 file

this file: d, d_cvg, upper_cutoff_cvg

let d section-local source, line 1093

Let d n := K * `|upper_moment (mu_ n) 1 w - upper_moment mu 1 w|.

Used by 3 declarations in 1 file

this file: d_cvg, upper_cutoff_cvg, upper_value_cvg

let d_cvg section-local source, line 1095

Let d_cvg : d n @[n --> \oo] --> 0.

lemma upper_cutoff_cvg main result source, line 1101

forall {R : realType} [mu_ : nat -> probability (measurableTypeR R) R]
  [mu : probability (measurableTypeR R) R],
(forall n : nat,
 (mu_ n).-integrable [set: measurableTypeR R] (EFin \o (fun x : R => (x : R) ^+ 2))) ->
mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => (x : R) ^+ 2)) ->
forall [c z : R],
-1 < c ->
upper_moment (mu_ n) 1 (upper_cutoff mu c z) @[n --> \oo] --> upper_moment mu 1
                                                              (upper_cutoff mu c z) ->
upper_cutoff (mu_ n) c z @[n --> \oo] --> upper_cutoff mu c z

Main result

Stated in the README together with upper_cutoff_stability.

Statement as written in the source

Lemma upper_cutoff_cvg : upper_cutoff (mu_ n) c z @[n --> \oo] --> w.

lemma upper_value_cvg main result source, line 1110

forall {R : realType} [mu_ : nat -> probability (measurableTypeR R) R]
  [mu : probability (measurableTypeR R) R],
(forall n : nat,
 (mu_ n).-integrable [set: measurableTypeR R] (EFin \o (fun x : R => (x : R) ^+ 2))) ->
mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => (x : R) ^+ 2)) ->
forall [c z : R],
-1 < c ->
upper_moment (mu_ n) 1 (upper_cutoff mu c z) @[n --> \oo] --> upper_moment mu 1
                                                              (upper_cutoff mu c z) ->
upper_moment (mu_ n) 2 (upper_cutoff mu c z) @[n --> \oo] --> upper_moment mu 2
                                                              (upper_cutoff mu c z) ->
upper_value (mu_ n) c z @[n --> \oo] --> upper_value mu c z

Main result

Stated in the README together with upper_cutoff_stability.

Statement as written in the source

Lemma upper_value_cvg :
  upper_value (mu_ n) c z @[n --> \oo] --> upper_value mu c z.

sectionsymmetric_law

Context {R : realType} (mu : probability (measurableTypeR R) R).
Hypothesis mu2 :
  mu.-integrable [set: measurableTypeR R] (EFin \o (fun x => (x : R) ^+ 2)).
Hypothesis musym : forall A : set (measurableTypeR R), measurable A ->
  mu ((fun x => - x) @^-1` A) = mu A.
Local Notation m := (upper_moment mu 1).
Local Notation s := (upper_moment mu 2).
Local Notation integrable f :=
  (mu.-integrable [set: measurableTypeR R] (EFin \o f)).

let mN section-local source, line 1150

Let mN : measurable_fun [set: measurableTypeR R]
  (fun x : measurableTypeR R => (- x : measurableTypeR R)).

Used by 2 declarations in 1 file

this file: integrable_sym, upper_variational_sym_le

lemma integrable_sym main result source, line 1154

forall {R : realType} [mu : probability (measurableTypeR R) R],
(forall A : set (measurableTypeR R),
 (((R.-ocitv).-measurable).-sigma).-measurable A -> mu ([eta -%R] @^-1` A) = mu A) ->
forall [f : measurableTypeR R -> R],
mu.-integrable [set: measurableTypeR R] (EFin \o f) ->
mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => f (- x)))

Main result

Stated in the README together with Rintegral_sqr_le.

Statement as written in the source

Lemma integrable_sym (f : measurableTypeR R -> R) :
  integrable f -> integrable (fun x => f (- x)).

Used by 5 declarations in 2 files

this file: Rintegral_sym, upper_variational_sym_le, clip_energyE
GaussianAnalysis.probability.clip_profile: integrable_upper1_reflect, clip_energy_shiftE

lemma Rintegral_sym main result source, line 1174

forall {R : realType} [mu : probability (measurableTypeR R) R],
(forall A : set (measurableTypeR R),
 (((R.-ocitv).-measurable).-sigma).-measurable A -> mu ([eta -%R] @^-1` A) = mu A) ->
forall [f : measurableTypeR R -> R],
mu.-integrable [set: measurableTypeR R] (EFin \o f) -> \int[mu]_x f (- x) = \int[mu]_x f x

Main result

Stated in the README together with Rintegral_sqr_le.

Statement as written in the source

Lemma Rintegral_sym (f : measurableTypeR R -> R) :
  integrable f -> \int[mu]_x f (- x) = \int[mu]_x f x.

Used by 6 declarations in 2 files

this file: Rintegral_id_sym, upper_reflect, upper_variational_sym_le, clip_energyE
GaussianAnalysis.probability.clip_profile: upper_moment1_reflect, clip_energy_shiftE

lemma Rintegral_id_sym source, line 1185

forall {R : realType} [mu : probability (measurableTypeR R) R],
mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => (x : R) ^+ 2)) ->
(forall A : set (measurableTypeR R),
 (((R.-ocitv).-measurable).-sigma).-measurable A -> mu ([eta -%R] @^-1` A) = mu A) ->
\int[mu]_x (x : R) = 0

Statement as written in the source

Lemma Rintegral_id_sym : \int[mu]_x (x : R) = 0.

Used by 4 declarations in 2 files

this file: upper_moment1_sym, upper_moment2_sym
GaussianAnalysis.probability.clip_profile: clip_res_sqE, clip_objectiveE

let upper_reflect section-local source, line 1194

Let upper_reflect k w : (k <= 2)%N ->
  upper_moment mu k (- w) = \int[mu]_x (Num.max (w - (x : R)) 0 ^+ k).

Used by 2 declarations in 1 file

this file: upper_moment1_sym, upper_moment2_sym

let integrable_reflect section-local source, line 1202

Let integrable_reflect k w : (k <= 2)%N ->
  integrable (fun x => Num.max (w - (x : R)) 0 ^+ k).

Used by 2 declarations in 1 file

this file: upper_moment1_sym, upper_moment2_sym

lemma upper_moment1_sym main result source, line 1219

forall {R : realType} [mu : probability (measurableTypeR R) R],
mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => (x : R) ^+ 2)) ->
(forall A : set (measurableTypeR R),
 (((R.-ocitv).-measurable).-sigma).-measurable A -> mu ([eta -%R] @^-1` A) = mu A) ->
forall w : R, upper_moment mu 1 (- w) = upper_moment mu 1 w + w

Main result, as the README states it

For a law invariant under x |-> -x with E X^2 = v: m(-w) = m(w) + w, s(-w) + s(w) = v + w^2, and for c > -1, c' = -c / (1 + c), z' = -z / (1 + c), the cutoff of (c', z') is minus that of (c, z) and the two values add up to v + z^2 / (1 + c) (the scalar part of Lemma 5.9); at z = 0 the variational bound holds without the positive part, (E X f(X))^2 <= value (E f(X)^2 + c (E f(X))^2) (Proposition 5.10 (ii)).

Statement as written in the source

Lemma upper_moment1_sym w : m (- w) = m w + w.

Used by 2 declarations in 1 file

this file: upper_cutoff_dual, upper_value_dual

lemma upper_moment2_sym main result source, line 1238

forall {R : realType} [mu : probability (measurableTypeR R) R],
mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => (x : R) ^+ 2)) ->
(forall A : set (measurableTypeR R),
 (((R.-ocitv).-measurable).-sigma).-measurable A -> mu ([eta -%R] @^-1` A) = mu A) ->
forall w : R,
upper_moment mu 2 (- w) + upper_moment mu 2 w = \int[mu]_x (x : R) ^+ 2 + w ^+ 2

Main result

Stated in the README together with upper_moment1_sym.

Statement as written in the source

Lemma upper_moment2_sym w : s (- w) + s w = \int[mu]_x ((x : R) ^+ 2) + w ^+ 2.

Used by 1 declaration in 1 file

this file: upper_value_dual

lemma upper_cutoff_dual main result source, line 1256

forall {R : realType} [mu : probability (measurableTypeR R) R],
mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => (x : R) ^+ 2)) ->
(forall A : set (measurableTypeR R),
 (((R.-ocitv).-measurable).-sigma).-measurable A -> mu ([eta -%R] @^-1` A) = mu A) ->
forall [c : join_Num_POrderZmodule_between_Algebra_BaseZmodule_and_Order_Preorder R]
  (z : join_Num_NumDomain_between_Order_Preorder_and_GRing_UnitRing R),
-1 < c -> upper_cutoff mu (- c / (1 + c)) (- z / (1 + c)) = - upper_cutoff mu c z

Main result

Stated in the README together with upper_moment1_sym.

Statement as written in the source

Lemma upper_cutoff_dual c z : -1 < c ->
  upper_cutoff mu (- c / (1 + c)) (- z / (1 + c)) = - upper_cutoff mu c z.

Used by 1 declaration in 1 file

this file: upper_value_dual

lemma upper_value_dual main result source, line 1271

forall {R : realType} [mu : probability (measurableTypeR R) R],
mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => (x : R) ^+ 2)) ->
(forall A : set (measurableTypeR R),
 (((R.-ocitv).-measurable).-sigma).-measurable A -> mu ([eta -%R] @^-1` A) = mu A) ->
forall [c : join_Num_POrderZmodule_between_Algebra_BaseZmodule_and_Order_Preorder R]
  (z : R),
-1 < c ->
upper_value mu c z + upper_value mu (- c / (1 + c)) (- z / (1 + c)) =
\int[mu]_x (x : R) ^+ 2 + z ^+ 2 / (1 + c)

Main result

Stated in the README together with upper_moment1_sym.

Statement as written in the source

Lemma upper_value_dual c z : -1 < c ->
  upper_value mu c z + upper_value mu (- c / (1 + c)) (- z / (1 + c)) =
  \int[mu]_x ((x : R) ^+ 2) + z ^+ 2 / (1 + c).

lemma upper_variational_sym_le main result source, line 1287

forall {R : realType} [mu : probability (measurableTypeR R) R],
mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => (x : R) ^+ 2)) ->
(forall A : set (measurableTypeR R),
 (((R.-ocitv).-measurable).-sigma).-measurable A -> mu ([eta -%R] @^-1` A) = mu A) ->
forall [c : join_Num_POrderZmodule_between_Algebra_BaseZmodule_and_Order_Preorder R]
  [f : measurableTypeR R -> R],
-1 < c ->
measurable_fun [set: measurableTypeR R] f ->
(forall x : measurableTypeR R, 0 <= f x) ->
mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : measurableTypeR R => f x ^+ 2)) ->
(\int[mu]_x ((x : R) * f x)) ^+ 2 <=
upper_value mu c 0 * (\int[mu]_x f x ^+ 2 + c * (\int[mu]_x f x) ^+ 2)

Main result

Stated in the README together with upper_moment1_sym.

Statement as written in the source

Lemma upper_variational_sym_le c (f : measurableTypeR R -> R) : -1 < c ->
  measurable_fun [set: measurableTypeR R] f -> (forall x, 0 <= f x) ->
  integrable (fun x => f x ^+ 2) ->
  (\int[mu]_x ((x : R) * f x)) ^+ 2 <=
  upper_value mu c 0 * (\int[mu]_x (f x ^+ 2) + c * (\int[mu]_x f x) ^+ 2).

HB declares canonical projections that the structures of the measure already provide; the warning says so. The setting lasts until the end of this file and is not exported.

Set Warnings "-redundant-canonical-projection".

sectionempirical

Context {R : realType}.
Local Open Scope ereal_scope.
Implicit Types (s : seq R) (A : set (measurableTypeR R)).

definition emp_diracs source, line 1336

Type

forall {R : realType}, seq R -> nat -> measure (measurableTypeR R) R

Definition

Definition emp_diracs s (k : nat) :
    {measure set (measurableTypeR R) -> \bar R} :=
  \d_(nth 0%R s k : measurableTypeR R).

The Dirac masses at the elements of s.

Used by 2 declarations in 1 file

this file: empirical, ge0_integral_empirical

lemma emp_weight_ge0 source, line 1340

forall {R : realType} (s : seq R), (0 : R) <= ((size s)%:R^-1 : R)

Statement as written in the source

Lemma emp_weight_ge0 s : (0 <= (size s)%:R^-1 :> R)%R.

Used by 1 declaration in 1 file

this file: empirical

definition empirical main result source, line 1345

Type

forall {R : realType}, seq R -> set (measurableTypeR R) -> \bar R

Definition

Definition empirical s : set (measurableTypeR R) -> \bar R :=
  if s is [::] then \d_(0%R : measurableTypeR R)
  else mscale (NngNum (emp_weight_ge0 s)) (msum (emp_diracs s) (size s)).

The empirical law of s: the average of the Dirac masses at its elements, and the Dirac mass at 0 when s is empty.

Main result, as the README states it

The empirical law of a nonempty list s of reals, the average of the Dirac masses at its elements, is a probability on the line; integrals against it are averages over s, so the upper partial moments of the empirical law of g_1, ..., g_d are (1/d) sum_i (g_i - w)_+^k.

Used by 12 declarations in 1 file

this file: empiricalE, empirical0, empirical_ge0, empirical_sigma_additive, instance at line 1368, empirical_setT, instance at line 1380, ge0_integral_empirical, integrable_empirical, Rintegral_empirical_ge0, Rintegral_empirical, empirical_fun

lemma empiricalE source, line 1349

forall {R : realType} [s : seq R] (A : set (measurableTypeR R)),
s != [::] ->
empirical s A = (((size s)%:R^-1)%:E * (\sum_(x <- s) \d_(x : measurableTypeR R) A)%R)%E

Statement as written in the source

Lemma empiricalE s A : s != [::] ->
  empirical s A =
  (((size s)%:R^-1)%R)%:E * \sum_(x <- s) \d_(x : measurableTypeR R) A.

Used by 1 declaration in 1 file

this file: empirical_setT

let empirical0 section-local source, line 1359

Let empirical0 s : empirical s set0 = 0.

Used by 1 declaration in 1 file

this file: instance at line 1368

let empirical_ge0 section-local source, line 1362

Let empirical_ge0 s A : 0 <= empirical s A.

Used by 1 declaration in 1 file

this file: instance at line 1368

let empirical_sigma_additive section-local source, line 1365

Let empirical_sigma_additive s : semi_sigma_additive (empirical s).

Used by 1 declaration in 1 file

this file: instance at line 1368

instance instance at line 1368 source, line 1368

HB.instance Definition _ s := isMeasure.Build _ _ _ (empirical s)
  (empirical0 s) (empirical_ge0 s) (@empirical_sigma_additive s).

lemma empirical_setT main result source, line 1371

forall {R : realType} (s : seq R), empirical s [set: measurableTypeR R] = 1%E

Main result

Stated in the README together with empirical.

Statement as written in the source

Lemma empirical_setT s : empirical s [set: measurableTypeR R] = 1.

Used by 1 declaration in 1 file

this file: instance at line 1380

instance instance at line 1380 source, line 1380

HB.instance Definition _ s :=
  Measure_isProbability.Build _ _ _ (empirical s) (empirical_setT s).

lemma ge0_integral_empirical main result source, line 1384

forall {R : realType} [s : seq R] [f : measurableTypeR R -> \bar R],
s != [::] ->
measurable_fun [set: measurableTypeR R] f ->
(forall x : measurableTypeR R, (0%R <= f x)%E) ->
(\int[empirical s]_x f x)%E = (((size s)%:R^-1)%:E * (\sum_(x <- s) f x)%R)%E

Main result

Stated in the README together with empirical.

Statement as written in the source

Lemma ge0_integral_empirical s (f : measurableTypeR R -> \bar R) :
  s != [::] -> measurable_fun [set: measurableTypeR R] f ->
  (forall x, 0 <= f x) ->
  \int[empirical s]_x f x = (((size s)%:R^-1)%R)%:E * \sum_(x <- s) f x.

Used by 2 declarations in 1 file

this file: integrable_empirical, Rintegral_empirical_ge0

lemma integrable_empirical main result source, line 1395

forall {R : realType} [s : seq R] [f : measurableTypeR R -> R],
s != [::] ->
measurable_fun [set: measurableTypeR R] f ->
(empirical s).-integrable [set: measurableTypeR R] (EFin \o f)

Main result

Stated in the README together with empirical.

Statement as written in the source

Lemma integrable_empirical s (f : measurableTypeR R -> R) :
  s != [::] -> measurable_fun [set: measurableTypeR R] f ->
  (empirical s).-integrable [set: measurableTypeR R] (EFin \o f).

Used by 2 declarations in 1 file

this file: Rintegral_empirical, empirical_fun_sqr

lemma Rintegral_empirical_ge0 source, line 1407

forall {R : realType} [s : seq R] [f : measurableTypeR R -> R],
s != [::] ->
measurable_fun [set: measurableTypeR R] f ->
(forall x : measurableTypeR R, 0 <= f x) ->
\int[empirical s]_x f x = (size s)%:R^-1 * \sum_(x <- s) f x

Statement as written in the source

Lemma Rintegral_empirical_ge0 s (f : measurableTypeR R -> R) :
  s != [::] -> measurable_fun [set: measurableTypeR R] f ->
  (forall x, (0 <= f x)%R) ->
  (\int[empirical s]_x f x = (size s)%:R^-1 * \sum_(x <- s) f x)%R.

Used by 1 declaration in 1 file

this file: Rintegral_empirical

lemma Rintegral_empirical main result source, line 1419

forall {R : realType} [s : seq R] [f : measurableTypeR R -> R],
s != [::] ->
measurable_fun [set: measurableTypeR R] f ->
\int[empirical s]_x f x = (size s)%:R^-1 * \sum_(x <- s) f x

Main result

Stated in the README together with empirical.

Statement as written in the source

Lemma Rintegral_empirical s (f : measurableTypeR R -> R) :
  s != [::] -> measurable_fun [set: measurableTypeR R] f ->
  (\int[empirical s]_x f x = (size s)%:R^-1 * \sum_(x <- s) f x)%R.

Used by 1 declaration in 1 file

this file: Rintegral_empirical_fun

sectionempirical_variational

Context {R : realType} (d : nat) (g : 'I_d -> R).
Hypothesis d0 : (0 < d)%N.

definition empirical_fun main result source, line 1452

Type

forall {R : realType} [d : nat], ('I_d -> R) -> set (measurableTypeR R) -> \bar R

Definition

Definition empirical_fun := empirical [seq g i | i <- enum 'I_d].

The empirical law of g 0, ..., g (d - 1).

Main result

Stated in the README together with empirical.

Used by 5 declarations in 1 file

this file: Rintegral_empirical_fun, empirical_fun_sqr, upper_moment_empirical_fun, empirical_variational_le, empirical_variational_attained

Local Notation nu := empirical_fun.

lemma empirical_fun_neq0 source, line 1456

forall {R : realType} [d : nat] (g : 'I_d -> R),
(0 < d)%N -> [seq g i | i <- enum 'I_d] != [::]

Statement as written in the source

Lemma empirical_fun_neq0 : [seq g i | i <- enum 'I_d] != [::].

Used by 2 declarations in 1 file

this file: Rintegral_empirical_fun, empirical_fun_sqr

lemma sum_empirical_fun source, line 1459

forall {R : realType} [d : nat] (g : 'I_d -> R) (F : R -> R),
\sum_(x <- [seq g i | i <- enum 'I_d]) F x = \sum_i F (g i)

Statement as written in the source

Lemma sum_empirical_fun (F : R -> R) :
  \sum_(x <- [seq g i | i <- enum 'I_d]) F x = \sum_i F (g i).

Used by 1 declaration in 1 file

this file: Rintegral_empirical_fun

lemma Rintegral_empirical_fun source, line 1463

forall {R : realType} [d : nat] (g : 'I_d -> R),
(0 < d)%N ->
forall [f : measurableTypeR R -> R],
measurable_fun [set: measurableTypeR R] f ->
\int[empirical_fun g]_x f x = d%:R^-1 * \sum_i f (g i)

Statement as written in the source

Lemma Rintegral_empirical_fun (f : measurableTypeR R -> R) :
  measurable_fun [set: measurableTypeR R] f ->
  \int[nu]_x f x = d%:R^-1 * \sum_i f (g i).

Used by 2 declarations in 1 file

this file: upper_moment_empirical_fun, empirical_variational_attained

lemma empirical_fun_sqr source, line 1471

forall {R : realType} [d : nat] (g : 'I_d -> R),
(0 < d)%N ->
(empirical_fun g).-integrable [set: measurableTypeR R]
  (EFin \o (fun x : R => (x : R) ^+ 2))

Statement as written in the source

Lemma empirical_fun_sqr :
  nu.-integrable [set: measurableTypeR R] (EFin \o (fun x => (x : R) ^+ 2)).

Used by 2 declarations in 1 file

this file: empirical_variational_le, empirical_variational_attained

lemma upper_moment_empirical_fun main result source, line 1478

forall {R : realType} [d : nat] (g : 'I_d -> R),
(0 < d)%N ->
forall (k : nat) (w : R),
upper_moment (empirical_fun g) k w = d%:R^-1 * \sum_i maxr (g i - w) 0 ^+ k

Main result

Stated in the README together with empirical.

Statement as written in the source

Lemma upper_moment_empirical_fun k w :
  upper_moment nu k w = d%:R^-1 * \sum_i Num.max (g i - w) 0 ^+ k.

Used by 1 declaration in 1 file

this file: empirical_variational_le

lemma empirical_variational_le main result source, line 1488

forall {R : realType} [d : nat] (g : 'I_d -> R),
(0 < d)%N ->
forall [c : R] (z : R) [r : 'I_d -> R],
0 <= c ->
(forall i : 'I_d, 0 <= r i) ->
d%:R^-1 * \sum_i (g i + z) * r i <=
Num.ExtraDef.sqrtr (upper_value (empirical_fun g) c z) *
Num.ExtraDef.sqrtr (d%:R^-1 * \sum_i r i ^+ 2 + c * (d%:R^-1 * \sum_i r i) ^+ 2)

The finite form of Lemma 5.7: the weights need not be functions of the values g i.

Main result, as the README states it

The finite form of Lemma 5.7 of Koehler and Sohn for c >= 0, with weights that need not be functions of the values: for r_i >= 0, (1/d) sum_i (g_i + z) r_i <= sqrt V ((1/d) sum_i r_i^2 + c ((1/d) sum_i r_i)^2)^(1/2), V the value of the empirical law of the g_i, with equality at r_i = (g_i - w)_+, w the cutoff.

Statement as written in the source

Lemma empirical_variational_le (c z : R) (r : 'I_d -> R) :
  0 <= c -> (forall i, 0 <= r i) ->
  d%:R^-1 * \sum_i (g i + z) * r i <=
  Num.sqrt (upper_value nu c z) *
  Num.sqrt (d%:R^-1 * \sum_i r i ^+ 2 + c * (d%:R^-1 * \sum_i r i) ^+ 2).

lemma empirical_variational_attained main result source, line 1559

forall {R : realType} [d : nat] (g : 'I_d -> R),
(0 < d)%N ->
forall [c : R] (z : R),
-1 < c ->
d%:R^-1 * \sum_i (g i + z) * maxr (g i - upper_cutoff (empirical_fun g) c z) 0 =
upper_value (empirical_fun g) c z

Main result

Stated in the README together with empirical_variational_le.

Statement as written in the source

Lemma empirical_variational_attained (c z : R) : -1 < c ->
  d%:R^-1 * \sum_i (g i + z) * Num.max (g i - upper_cutoff nu c z) 0 =
  upper_value nu c z.

Monotonicity from a Taylor bound

sectiontaylor_monotone

Context {R : realType}.

lemma taylor_nincr main result source, line 1579

forall {R : realType} [F g : R -> R] [K a b : R],
(forall t h : R, 0 <= h -> `|F (t + h) - F t - h * g t| <= K * h ^+ 2) ->
a <= b -> (forall t : R, a <= t -> t < b -> g t <= 0) -> F b <= F a

A function with derivative g in the sense of a Taylor bound with a quadratic remainder does not increase where g <= 0: a discrete integration of the bound.

Main result

Stated in the README together with clip_energy.

Statement as written in the source

Lemma taylor_nincr (F g : R -> R) (K a b : R) :
  (forall t h : R, 0 <= h -> `|F (t + h) - F t - h * g t| <= K * h ^+ 2) ->
  a <= b -> (forall t : R, a <= t -> t < b -> g t <= 0) -> F b <= F a.

Used by 2 declarations in 1 file

this file: taylor_ndecr, clip_value_attained

lemma taylor_ndecr main result source, line 1625

forall {R : realType} [F g : R -> R] [K a b : R],
(forall t h : R, 0 <= h -> `|F (t + h) - F t - h * g t| <= K * h ^+ 2) ->
a <= b -> (forall t : R, a <= t -> t < b -> 0 <= g t) -> F a <= F b

Main result

Stated in the README together with clip_energy.

Statement as written in the source

Lemma taylor_ndecr (F g : R -> R) (K a b : R) :
  (forall t h : R, 0 <= h -> `|F (t + h) - F t - h * g t| <= K * h ^+ 2) ->
  a <= b -> (forall t : R, a <= t -> t < b -> 0 <= g t) -> F a <= F b.

Used by 1 declaration in 1 file

this file: clip_value_attained

The energy of a clip to [t, C t]

sectionclip_energy

Context {R : realType} (mu : probability (measurableTypeR R) R).
Hypothesis mu2 :
  mu.-integrable [set: measurableTypeR R] (EFin \o (fun x => (x : R) ^+ 2)).
Local Notation m := (upper_moment mu 1).
Local Notation s := (upper_moment mu 2).

definition clip_energy main result source, line 1656

Type

forall {R : realType}, probability (measurableTypeR R) R -> R -> R -> R

Definition

Definition clip_energy (C t : R) : R := s (- t) + s (C * t).

s(-t) + s(C t): for a symmetric law, the mean of (t - X)_+^2 + (X - C t)_+^2 (clip_energyE), which is the mean squared distance from X to the interval [t, C t] when t <= C t, in particular for C >= 1 and t >= 0.

Main result, as the README states it

For a law with a finite second moment, clip_energy mu C t = s(-t) + s(C t), which for a symmetric law is the mean of (t - X)_+^2 + (X - C t)_+^2, the mean squared distance from X to [t, C t] when t <= C t (for example C >= 1 and t >= 0), and its infimum clip_value mu C over t >= 0. Its derivative in t is 2 (m(-t) - C m(C t)) (a Taylor bound with remainder (1 + C^2) h^2), so a t0 >= 0 where the derivative is <= 0 before and >= 0 after is a minimum. It is nonincreasing in C, with 0 <= clip_energy C t - clip_energy C' t <= (C' - C) t (m(C t) + m(C' t)) for C <= C'. The tool: a function with |F(t + h) - F(t) - h g(t)| <= K h^2 for h >= 0 is nonincreasing where g <= 0 and nondecreasing where g >= 0.

Used by 8 declarations in 1 file

this file: clip_value, clip_energy_ge0, clip_value_le, clip_value_ge, clip_energy_taylor, clip_value_attained, clip_energy_C, clip_energyE

definition clip_value main result source, line 1659

Type

forall {R : realType}, probability (measurableTypeR R) R -> R -> R

Definition

Definition clip_value (C : R) : R :=
  inf [set clip_energy C t | t in [set t : R | 0 <= t]].

Its infimum over t >= 0.

Main result

Stated in the README together with clip_energy.

Used by 4 declarations in 1 file

this file: clip_value_le, clip_value_ge, clip_value_attained, clip_value_nincr

lemma clip_energy_ge0 source, line 1662

forall {R : realType} (mu : probability (measurableTypeR R) R) (C t : R),
0 <= clip_energy mu C t

Statement as written in the source

Lemma clip_energy_ge0 (C t : R) : 0 <= clip_energy C t.

Used by 1 declaration in 1 file

this file: clip_value_le

lemma clip_value_le source, line 1665

forall {R : realType} (mu : probability (measurableTypeR R) R) (C : R) [t : R],
0 <= t -> clip_value mu C <= clip_energy mu C t

Statement as written in the source

Lemma clip_value_le (C t : R) : 0 <= t -> clip_value C <= clip_energy C t.

Used by 2 declarations in 1 file

this file: clip_value_attained, clip_value_nincr

lemma clip_value_ge source, line 1671

forall {R : realType} [mu : probability (measurableTypeR R) R] [C r : R],
(forall t : R, 0 <= t -> r <= clip_energy mu C t) -> r <= clip_value mu C

Statement as written in the source

Lemma clip_value_ge (C r : R) :
  (forall t : R, 0 <= t -> r <= clip_energy C t) -> r <= clip_value C.

Used by 2 declarations in 1 file

this file: clip_value_attained, clip_value_nincr

lemma clip_energy_taylor main result source, line 1679

forall {R : realType} [mu : probability (measurableTypeR R) R],
mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => (x : R) ^+ 2)) ->
forall C t h : R,
`|clip_energy mu C (t + h) - clip_energy mu C t -
  h * (2 * (upper_moment mu 1 (- t) - C * upper_moment mu 1 (C * t)))| <=
(1 + C ^+ 2) * h ^+ 2

The derivative in t is 2 (m(-t) - C m(C t)).

Main result

Stated in the README together with clip_energy.

Statement as written in the source

Lemma clip_energy_taylor (C t h : R) :
  `|clip_energy C (t + h) - clip_energy C t -
    h * (2 * (m (- t) - C * m (C * t)))| <= (1 + C ^+ 2) * h ^+ 2.

Used by 1 declaration in 1 file

this file: clip_value_attained

lemma clip_value_attained main result source, line 1698

forall {R : realType} [mu : probability (measurableTypeR R) R],
mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => (x : R) ^+ 2)) ->
forall [C t0 : R],
0 <= t0 ->
(forall t : R, 0 <= t -> t < t0 -> upper_moment mu 1 (- t) <= C * upper_moment mu 1 (C * t)) ->
(forall t : R, t0 <= t -> C * upper_moment mu 1 (C * t) <= upper_moment mu 1 (- t)) ->
clip_value mu C = clip_energy mu C t0

A zero t0 of the derivative, with the derivative <= 0 before it and >= 0 after it, is a minimum.

Main result

Stated in the README together with clip_energy.

Statement as written in the source

Lemma clip_value_attained (C t0 : R) : 0 <= t0 ->
  (forall t : R, 0 <= t -> t < t0 -> m (- t) <= C * m (C * t)) ->
  (forall t : R, t0 <= t -> C * m (C * t) <= m (- t)) ->
  clip_value C = clip_energy C t0.

lemma clip_energy_C main result source, line 1717

forall {R : realType} [mu : probability (measurableTypeR R) R],
mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => (x : R) ^+ 2)) ->
forall [C C' t : R],
0 <= t ->
C <= C' ->
0 <= clip_energy mu C t - clip_energy mu C' t <=
(C' - C) * t * (upper_moment mu 1 (C * t) + upper_moment mu 1 (C' * t))

Main result

Stated in the README together with clip_energy.

Statement as written in the source

Lemma clip_energy_C (C C' t : R) : 0 <= t -> C <= C' ->
  0 <= clip_energy C t - clip_energy C' t <=
    (C' - C) * t * (m (C * t) + m (C' * t)).

Used by 1 declaration in 1 file

this file: clip_value_nincr

lemma clip_value_nincr main result source, line 1728

forall {R : realType} [mu : probability (measurableTypeR R) R],
mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => (x : R) ^+ 2)) ->
forall [C C' : R], C <= C' -> clip_value mu C' <= clip_value mu C

Main result

Stated in the README together with clip_energy.

Statement as written in the source

Lemma clip_value_nincr (C C' : R) : C <= C' -> clip_value C' <= clip_value C.

sectionclip_energy_sym

Context {R : realType} (mu : probability (measurableTypeR R) R).
Hypothesis mu2 :
  mu.-integrable [set: measurableTypeR R] (EFin \o (fun x => (x : R) ^+ 2)).
Hypothesis musym : forall A : set (measurableTypeR R), measurable A ->
  mu ((fun x => - x) @^-1` A) = mu A.

lemma clip_energyE main result source, line 1747

forall {R : realType} [mu : probability (measurableTypeR R) R],
mu.-integrable [set: measurableTypeR R] (EFin \o (fun x : R => (x : R) ^+ 2)) ->
(forall A : set (measurableTypeR R),
 (((R.-ocitv).-measurable).-sigma).-measurable A -> mu ([eta -%R] @^-1` A) = mu A) ->
forall C t : R,
\int[mu]_x (maxr (t - (x : R)) 0 ^+ 2 + maxr ((x : R) - C * t) 0 ^+ 2) = clip_energy mu C t

For a symmetric law, clip_energy is the integral of (t - x)_+^2 + (x - C t)_+^2, the squared distance from x to [t, C t] when 0 <= t <= C t.

Main result

Stated in the README together with clip_energy.

Statement as written in the source

Lemma clip_energyE (C t : R) :
  \int[mu]_x (Num.max (t - (x : R)) 0 ^+ 2 + Num.max ((x : R) - C * t) 0 ^+ 2) =
  clip_energy mu C t.

Generated from commit 9046883 (tag phase12) of the ellipsoid fitting repository. Signatures are printed by Rocq 9.1.1; links in the source statements come from the compiled .glob files. The source links open the files on GitHub at this commit, in the now-public repository.