CavityCutoffTests.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Bounded-test cutoff removal, including a zero restricted normalizer, and the good-compression/bad-compression split for the full-system tail.

theorem OAI.InvariantIsing.cavity_conditioning_bound_all line 14

theorem OAI.InvariantIsing.cavity_twoReplica_cutoff_bound line 32

Source documentation

Restricting both replicas changes a bounded test by at most four times its bound times the discarded one-replica mass.

theorem cavity_twoReplica_cutoff_bound {X : Type*} [MeasurableSpace X]
    (μ : Measure X) [IsProbabilityMeasure μ] (s : Set X) (hs : MeasurableSet s)
    (f : (Fin 2 → X) → ℝ) (hf : Integrable f (Measure.pi (fun _ : Fin 2 => μ)))
    {M : ℝ} (hM : 0 ≤ M) (hb : ∀ x, |f x| ≤ M) :
    |(∫ x, f x ∂cond (Measure.pi (fun _ : Fin 2 => μ)) (univ.pi (fun _ => s))) -
      ∫ x, f x ∂Measure.pi (fun _ : Fin 2 => μ)| ≤ 4 * M * μ.real sᶜ := by
…

theorem OAI.InvariantIsing.cavity_full_radial_tail line 53

Source documentation

On the good compression event it suffices to dominate the special projection norm by an integrable quantity. No inverse-Gram moment on the bad event is required.

theorem cavity_full_radial_tail {Ω : Type*} [MeasurableSpace Ω] {d : ℕ}
    (μ : Measure Ω) [IsProbabilityMeasure μ] (good : Set Ω)
    (y : Ω → EuclideanSpace ℝ (Fin d)) (T : Ω → ℝ)
    (hT : Integrable T μ) (hT0 : ∀ ω, 0 ≤ T ω)
    (hy : ∀ ω ∈ good, ‖y ω‖ ^ 2 ≤ T ω)
    {K B : ℝ} (hmean : (∫ ω, T ω ∂μ) ≤ K) (hB : 0 < B) :
    μ.real {ω | B < ‖y ω‖} ≤ μ.real goodᶜ + K / B ^ 2 := by
…