CavityFieldSelfConsistency.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The actual finite scalar fields satisfy the tied-fiber hypothesis away from their countably many grid endpoints.

lemma OAI.InvariantIsing.cavityFieldStep_height_on_rounded_cell line 16

theorem OAI.InvariantIsing.cavity_field_self_consistency_l1 line 31

Source documentation

Once the rounded cavity-spin tests converge, the actual scalar magnetization paths converge in L1. Grid endpoints need no convention.

theorem cavity_field_self_consistency_l1 (p : OverlapPath)
    (q : ℕ → OverlapPath) (h : ℕ → FieldStep) (height : ℕ → ℝ → ℝ)
    (hheight : ∀ n i s, s ∈ Ioo ((h n).cut i.castSucc) ((h n).cut i.succ) →
      (h n).height i = height n (p s))
    (hq : ∀ᵐ s ∂pathMeasure, Tendsto (fun n => q n s) atTop (𝓝 (p s)))
    (htest : ∀ Φ : ℝ →ᵇ ℝ, Tendsto
      (fun n => ∫ s, Φ (q n s) * (fieldMagnetizationPath (h n) s - q n s) ∂pathMeasure)
      atTop (𝓝 0)) :
    Tendsto (fun n => ∫ s, |fieldMagnetizationPath (h n) s - p s| ∂pathMeasure)
      atTop (𝓝 0) := by
…

Mentions: OAI.InvariantIsing.OverlapPath, OAI.InvariantIsing.FieldStep, OAI.InvariantIsing.fieldMagnetizationPath