FieldMajorantGaussian.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The sharp one-step Gaussian estimate for the entropy-domain majorant.

lemma OAI.InvariantIsing.log_moment_div_mono line 14

Source documentation

Positive logarithmic means increase with their exponent.

lemma log_moment_div_mono {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω)
    [IsProbabilityMeasure μ] {F : Ω → ℝ}
    (he : ∀ t : ℝ, Integrable (fun x => Real.exp (t * F x)) μ)
    {a d : ℝ} (ha : 0 < a) (had : a ≤ d) :
    a⁻¹ * Real.log (∫ x, Real.exp (a * F x) ∂μ) ≤
      d⁻¹ * Real.log (∫ x, Real.exp (d * F x) ∂μ) := by
…

lemma OAI.InvariantIsing.mean_le_log_moment_div line 36

Source documentation

Jensen at exponent zero, under the same actual moment assumptions.

lemma mean_le_log_moment_div {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω)
    [IsProbabilityMeasure μ] {F : Ω → ℝ} (hi : Integrable F μ)
    {d : ℝ} (hd : 0 < d) (he : Integrable (fun x => Real.exp (d * F x)) μ) :
    (∫ x, F x ∂μ) ≤ d⁻¹ * Real.log (∫ x, Real.exp (d * F x) ∂μ) := by
…

lemma OAI.InvariantIsing.fieldMajorant_gaussian_moment_bound line 48
lemma OAI.InvariantIsing.gaussianOperator_fieldMajorant_high line 96
lemma OAI.InvariantIsing.gaussianOperator_fieldMajorant line 111
Source documentation
The exact estimate (fld:majorant), including the zero-exponent root step.
```
lemma gaussianOperator_fieldMajorant {d a v : ℝ} (hd : 0 < d) (ha : 0 ≤ a)
    (hv : 0 ≤ v) (z : ℝ) :
    gaussianOperator a v (fieldMajorant d) z ≤
      fieldMajorant d z + max a d * v / 2 := by
…
```
Mentions: OAI.InvariantIsing.gaussianOperator, OAI.InvariantIsing.fieldMajorant