ScheduledSelection.lean`

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.DilutedSpinGlass.DepthAverage.average_le_const line 12
theorem OAI.DilutedSpinGlass.UniversalDictionary.scheduled_joint_selection line 37
Source documentation
One chosen physical sequence works for EVERY finite depth-coordinate alphabet and every assignment-dependent signed matrix experiment. In particular passing to a proper child's topology does not reselect the reservoir or its perturbation. The base case is the same scheduled family as the multileaf step and regular child fiber estimates.
```
theorem scheduled_joint_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 : ℕ → Spec L×ℕ → ℝ), StrictMono Ns ∧
      (∀ n i, us n i ∈ Icc (probeLow i.2) (probeHigh i.2)) ∧
      (∀ n, ConcreteReservoir.increment (weights L) prior (gridExponents L) direction anchor M (Ns n) (us n)≤
        liminf (pressure M) atTop+ε) ∧
      (∀ η : ℝ, 0<η → ∀ t : ℝ, 0<t → ∀ᶠ n in atTop,
        DepthAverage.average (regularShapeDomain .leaf (L+1) η)
…
```
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.DepthAverage.average