RegularCovarianceConvergence.lean`

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.DilutedSpinGlass.UniversalDictionary.grid_inverse_tendsto line 14
lemma OAI.DilutedSpinGlass.UniversalDictionary.eventually_large_grid line 17
theorem OAI.DilutedSpinGlass.UniversalDictionary.physicalShapeLimsup_tendsto line 28
Source documentation
Structural, finite-topology closure of the covariance recursion. The same physical selection is used for every child, with N taken to infinity before the mesh is refined.
```
theorem physicalShapeLimsup_tendsto (M : Model p) (θB hB : ℝ)
    (Ns : ℕ → ℕ → ℕ) (us : (L : ℕ) → ℕ → Spec L×ℕ → ℝ)
    (hcontrol : ∀ L, ScheduledControl M θB hB L (Ns L) (us L))
    (S : ReducedTopology) {η : ℝ} (hη : 0<η) :
    Tendsto (fun L => physicalShapeLimsup M θB hB L (Ns L) (us L) S η) atTop (𝓝 0) := by
…
```
Mentions: OAI.DilutedSpinGlass.Model, OAI.DilutedSpinGlass.UniversalDictionary.Spec, OAI.DilutedSpinGlass.UniversalDictionary.ScheduledControl, OAI.DilutedSpinGlass.ReducedTopology, OAI.DilutedSpinGlass.UniversalDictionary.physicalShapeLimsup
theorem OAI.DilutedSpinGlass.UniversalDictionary.physical_regular_covariance_selection line 66
Source documentation
A model-produced common controlling sequence for covariance concentration, including the low cavity increment required by the lower comparison. No concentration or selection hypothesis is added to the bounded model.
```
theorem physical_regular_covariance_selection (M : Model p) {C H : ℝ} (hC : 0≤C) (hH : 0≤H)
    (hθ : ∀ᵐ z ∂M.disorder.toMeasure, ∀ σ, |z.1 σ|≤C)
    (hh : ∀ᵐ h ∂M.field.toMeasure, |h|≤H)
    (hθi : Integrable (fun z : InteractionSample p => ‖z.1‖) M.disorder.toMeasure)
    (hhi : Integrable (fun h : ℝ => |h|) M.field.toMeasure)
    {ε : ℝ} (hε : 0<ε) :
    ∃ (Ns : ℕ → ℕ → ℕ) (us : (L : ℕ) → ℕ → Spec L×ℕ → ℝ),
      (∀ L, StrictMono (Ns L)) ∧
      (∀ L n i, us L n i ∈ Icc (probeLow i.2) (probeHigh i.2)) ∧
      (∀ L n, ConcreteReservoir.increment (weights L) prior (gridExponents L) direction anchor M (Ns L n) (us L n)≤
        liminf (pressure M) atTop+ε) ∧
      (∀ L, ScheduledControl M C H L (Ns L) (us L)) ∧
…
```
Mentions: OAI.DilutedSpinGlass.Model, OAI.DilutedSpinGlass.InteractionSample, OAI.DilutedSpinGlass.UniversalDictionary.Spec, OAI.DilutedSpinGlass.probeLow, OAI.DilutedSpinGlass.probeHigh, OAI.DilutedSpinGlass.ConcreteReservoir.increment, OAI.DilutedSpinGlass.UniversalDictionary.weights, OAI.DilutedSpinGlass.UniversalDictionary.prior, OAI.DilutedSpinGlass.UniversalDictionary.gridExponents, OAI.DilutedSpinGlass.UniversalDictionary.direction, OAI.DilutedSpinGlass.UniversalDictionary.anchor, OAI.DilutedSpinGlass.pressure, OAI.DilutedSpinGlass.UniversalDictionary.ScheduledControl