OAI/Probability/InvariantIsing/Gaussian/BaseGaussianVariance.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.InvariantIsing.cylinder_cgf_memLp_two line 14
2. lemma OAI.InvariantIsing.cylinder_log_partition_base line 38

   Source documentation

   Splitting off a fixed integrable base energy is an almost-everywhere identity for the actual countable Gaussian partition, including nonuniform and cascade-leaf weights.

   lemma cylinder_log_partition_base {X : Type*} [MeasurableSpace X] [Countable X]
       [MeasurableSingletonClass X] (ν : Measure X) [IsProbabilityMeasure ν]
       (H : X → ℝ) (hH : Integrable (fun x => Real.exp (H x)) ν)
       (A : X → ℕ →₀ ℝ) {B : ℝ} (hA : ∀ x, (A x).sum (fun _ c => c ^ 2) ≤ B) (t : ℝ) :
       (fun g : ℕ → ℝ => Real.log (∫ x, Real.exp (H x + t * cylinderField (A x) g) ∂ν))
         =ᵐ[gaussianCoordinates]
       (fun g => Real.log (∫ x, Real.exp (H x) ∂ν) +
         cgf (fun x => cylinderField (A x) g) (ν.tilted H) t) := by
   …

3. lemma OAI.InvariantIsing.cylinder_log_partition_memLp_two line 66
4. theorem OAI.InvariantIsing.countable_cylinder_log_partition_variance_le line 81

   Source documentation

   The actual countable Gaussian partition with arbitrary integrable base energy has the same coefficient variance bound. This is conditional only on the specified published Gaussian Poincaré consequence.

   theorem countable_cylinder_log_partition_variance_le (hpub : GaussianLipschitzVarianceInput)
       {X : Type*} [MeasurableSpace X] [Countable X] [MeasurableSingletonClass X]
       (ν : Measure X) [IsProbabilityMeasure ν] (H : X → ℝ)
       (hH : Integrable (fun x => Real.exp (H x)) ν)
       (A : X → ℕ →₀ ℝ) (B : ℝ) (hB : 0 ≤ B)
       (hA : ∀ x, (A x).sum (fun _ c => c ^ 2) ≤ B) (t : ℝ) :
       variance (fun g : ℕ → ℝ => Real.log
         (∫ x, Real.exp (H x + t * cylinderField (A x) g) ∂ν)) gaussianCoordinates ≤ t ^ 2 * B := by
   …

   Mentions: OAI.InvariantIsing.GaussianLipschitzVarianceInput