OAI/Probability/InvariantIsing/Gaussian/CountableGaussianComparison.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.InvariantIsing.finite_cylinder_mean_increment_le line 15
2. lemma OAI.InvariantIsing.cylinder_cgf_restriction_mean_tendsto line 65
3. theorem OAI.InvariantIsing.countable_cylinder_mean_increment_le line 83

   Source documentation

   The finite Gaussian mean estimate passes to countable leaf priors. The two endpoint variance caps ensure convergence of their actual means.

   theorem countable_cylinder_mean_increment_le {X : Type*} [MeasurableSpace X] [Countable X]
       [MeasurableSingletonClass X] (ν : Measure X) [IsProbabilityMeasure ν]
       (C A : X → ℕ →₀ ℝ) {B₀ B₁ K : ℝ}
       (hC : ∀ x, (C x).sum (fun _ c => c ^ 2) ≤ B₀)
       (hCA : ∀ x, (C x + A x).sum (fun _ c => c ^ 2) ≤ B₁)
       (hK : ∀ s ∈ Set.Icc (0 : ℝ) 1, ∀ x y,
         |cylinderCross (A x) (C y + s • A y)| ≤ K) :
       |(∫ g : ℕ → ℝ, cgf (fun x => cylinderField (C x + A x) g) ν 1 ∂gaussianCoordinates) -
         ∫ g : ℕ → ℝ, cgf (fun x => cylinderField (C x) g) ν 1 ∂gaussianCoordinates| ≤ 2 * K := by
   …

4. lemma OAI.InvariantIsing.cylinder_log_partition_mean_base line 118
5. theorem OAI.InvariantIsing.countable_cylinder_log_mean_increment_le line 134

   Source documentation

   The Gaussian mean comparison holds with the actual deterministic base energy and any countable probability prior, including cascade-leaf weights.

   theorem countable_cylinder_log_mean_increment_le {X : Type*} [MeasurableSpace X] [Countable X]
       [MeasurableSingletonClass X] (ν : Measure X) [IsProbabilityMeasure ν]
       (H : X → ℝ) (hH : Integrable (fun x => Real.exp (H x)) ν)
       (C A : X → ℕ →₀ ℝ) {B₀ B₁ K : ℝ}
       (hC : ∀ x, (C x).sum (fun _ c => c ^ 2) ≤ B₀)
       (hCA : ∀ x, (C x + A x).sum (fun _ c => c ^ 2) ≤ B₁)
       (hK : ∀ s ∈ Set.Icc (0 : ℝ) 1, ∀ x y,
         |cylinderCross (A x) (C y + s • A y)| ≤ K) :
       |(∫ g : ℕ → ℝ, Real.log (∫ x, Real.exp (H x + cylinderField (C x + A x) g) ∂ν)
           ∂gaussianCoordinates) -
         ∫ g : ℕ → ℝ, Real.log (∫ x, Real.exp (H x + cylinderField (C x) g) ∂ν)
           ∂gaussianCoordinates| ≤ 2 * K := by
   …

6. lemma OAI.InvariantIsing.cylinderCross_add_right line 151

   Distinct definitions of this name: OAI/Probability/InvariantIsing/Arrays/TensorWardCorrectionBound.lean:110 (same statement text; different proof or body). Qualify references as OAI.InvariantIsing.cylinderCross_add_right@path.

7. lemma OAI.InvariantIsing.cylinderCross_segment_bound line 158

   Source documentation

   Endpoint mixed-cross bounds control the whole coefficient segment.

   lemma cylinderCross_segment_bound {X : Type*} (A C : X → ℕ →₀ ℝ) {L : ℝ}
       (h₀ : ∀ x y, |cylinderCross (A x - C x) (C y)| ≤ L)
       (h₁ : ∀ x y, |cylinderCross (A x - C x) (A y)| ≤ L)
       {s : ℝ} (hs : s ∈ Set.Icc (0 : ℝ) 1) (x y : X) :
       |cylinderCross (A x - C x) (C y + s • (A y - C y))| ≤ L := by
   …

8. theorem OAI.InvariantIsing.countable_cylinder_log_mean_compare line 182

   Source documentation

   The form used for rotation comparison: any two bounded-variance coefficient families on the actual countable prior can be compared from mixed cross-covariances of their increment with the two endpoints.

   theorem countable_cylinder_log_mean_compare {X : Type*} [MeasurableSpace X] [Countable X]
       [MeasurableSingletonClass X] (ν : Measure X) [IsProbabilityMeasure ν]
       (H : X → ℝ) (hH : Integrable (fun x => Real.exp (H x)) ν)
       (A C : X → ℕ →₀ ℝ) {B₀ B₁ L : ℝ}
       (hC : ∀ x, (C x).sum (fun _ c => c ^ 2) ≤ B₀)
       (hA : ∀ x, (A x).sum (fun _ c => c ^ 2) ≤ B₁)
       (h₀ : ∀ x y, |cylinderCross (A x - C x) (C y)| ≤ L)
       (h₁ : ∀ x y, |cylinderCross (A x - C x) (A y)| ≤ L) :
       |(∫ g : ℕ → ℝ, Real.log (∫ x, Real.exp (H x + cylinderField (A x) g) ∂ν)
           ∂gaussianCoordinates) -
         ∫ g : ℕ → ℝ, Real.log (∫ x, Real.exp (H x + cylinderField (C x) g) ∂ν)
           ∂gaussianCoordinates| ≤ 2 * L := by
   …