OAI/Probability/DilutedSpin/ZeroShape.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DilutedSpinGlass.UniversalDictionary.physicalShapeCovariance line 16

   Source documentation

   Literal exact prescribed-shape covariance, using the original physical site mean at every signed extension of the complete tilted reservoir.

   noncomputable def physicalShapeCovariance (m : Fin (L+1) → ℝ)
       (S : PrescribedTree (L+1)) (anchorLeaf : S.Leaf)
       (M : Model p) (C H : ℝ) (N : ℕ) (u : Spec L×ℕ → ℝ)
       (F : (Option (Fin k) → Option (Fin k) → ℕ) → ℝ) (spinAnchor : Bool)
       (f : (S.Leaf → FinitePath (Fin N → Spin) (L+1)) → ℝ) : ℝ :=
   …

   Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.Model, OAI.DilutedSpinGlass.UniversalDictionary.Spec, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.Spin

2. lemma OAI.DilutedSpinGlass.UniversalDictionary.physicalShape_expansion line 28
3. theorem OAI.DilutedSpinGlass.UniversalDictionary.universal_shape_selection line 54

   Source documentation

   All exact finite prescribed constraints, not just pairwise sharing, hold on ONE physical low-increment sequence. The dictionary and its positive weights are fixed before selection and never changed by the tested shape.

   theorem universal_shape_selection (m : Fin (L+1) → ℝ)
       (M : Model p) {C H c : ℝ} (hC : 0 ≤ C) (hH : 0 ≤ H) (hc : 0 < c)
       (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)
       (hm : ∀ l, c ≤ m l) (hmono : Monotone m) (hend : m (Fin.last L) = 1)
       {ε : ℝ} (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 m direction anchor M (Ns n) (us n) ≤
           liminf (pressure M) atTop+ε) ∧
   …

   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.direction, OAI.DilutedSpinGlass.UniversalDictionary.anchor, OAI.DilutedSpinGlass.pressure

4. def OAI.DilutedSpinGlass.UniversalDictionary.zeroSpec line 98
5. lemma OAI.DilutedSpinGlass.UniversalDictionary.zeroSpec_anchor line 101
6. lemma OAI.DilutedSpinGlass.UniversalDictionary.shapeHistory_zero line 107
7. lemma OAI.DilutedSpinGlass.UniversalDictionary.externalShapeHistory_zero line 125
8. lemma OAI.DilutedSpinGlass.UniversalDictionary.shapeAverage_zero line 177
9. lemma OAI.DilutedSpinGlass.UniversalDictionary.shapeCovariance_zero line 197
10. lemma OAI.DilutedSpinGlass.UniversalDictionary.externalShapeHistory_singleton line 227
11. lemma OAI.DilutedSpinGlass.UniversalDictionary.shapeAverage_singleton line 243