OAI/Probability/DilutedSpin/FullRegularSelection.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DilutedSpinGlass.UniversalDictionary.gridExponents_pos line 14
2. structure OAI.DilutedSpinGlass.UniversalDictionary.FullShapeControl line 20

   Source documentation

   The full signed identity, retained for marker anchors as well as spin anchors. This is the literal output of the analytic perturbation selector.

   structure FullShapeControl (M : Model p) (C H : ℝ) (L : ℕ)
       (Ns : ℕ → ℕ) (us : ℕ → Spec L×ℕ → ℝ) : Prop where
   …

   Mentions: OAI.DilutedSpinGlass.Model, OAI.DilutedSpinGlass.UniversalDictionary.Spec

3. lemma OAI.DilutedSpinGlass.UniversalDictionary.FullShapeControl.matrix line 29
4. lemma OAI.DilutedSpinGlass.UniversalDictionary.FullShapeControl.singleton_energy line 50
5. lemma OAI.DilutedSpinGlass.UniversalDictionary.FullShapeControl.singleton_regular line 70
6. lemma OAI.DilutedSpinGlass.UniversalDictionary.physicalShapeAverage_le_of_pointwise line 99
7. lemma OAI.DilutedSpinGlass.UniversalDictionary.FullShapeControl.scheduled line 105
8. theorem OAI.DilutedSpinGlass.UniversalDictionary.full_regular_covariance_selection line 126

   Source documentation

   The stronger model-produced selection keeps all marker identities needed for the subsequent overlap concentration, without changing the sequence in the covariance induction.

   theorem full_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, FullShapeControl 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.FullShapeControl