OAI/Probability/InvariantIsing/Gaussian/GaussianBaseComparison.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.InvariantIsing.countable_cylinder_log_mean_cost line 17

   Source documentation

   An independent Gaussian perturbation changes the mean pressure by at most half its maximal variance, including after a fixed base-energy tilt.

   theorem countable_cylinder_log_mean_cost {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) :
       let d := (∫ g : ℕ → ℝ, Real.log (∫ x, Real.exp (H x + cylinderField (A x) g) ∂ν)
   …

2. lemma OAI.InvariantIsing.cylinder_partition_exp_integrable_ae line 29
3. theorem OAI.InvariantIsing.countable_cylinder_log_mean_base_compare line 48

   Source documentation

   A uniform deterministic energy change bounds the mean logpartition change, for every countable prior and bounded-variance Gaussian field.

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