OAI/Probability/DilutedSpin/ExternalRoot.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DilutedSpinGlass.ConcreteReservoir.integrable_scoreError line 19
2. def OAI.DilutedSpinGlass.ConcreteReservoir.spinFactor line 33
3. lemma OAI.DilutedSpinGlass.ConcreteReservoir.measurable_spinFactor line 38
4. lemma OAI.DilutedSpinGlass.ConcreteReservoir.abs_log_affine_le line 42
5. lemma OAI.DilutedSpinGlass.ConcreteReservoir.spinFactor_log_bound line 59
6. def OAI.DilutedSpinGlass.ConcreteReservoir.increment line 69

   Source documentation

   The increment of the actual quenched physical system with the complete Poisson dictionary, not a pressure-rate proxy. Its size is N+1.

   noncomputable def increment (M : Model p) (N : ℕ) (u : K×ℕ → ℝ) : ℝ :=
   …

   Mentions: OAI.DilutedSpinGlass.Model

7. lemma OAI.DilutedSpinGlass.ConcreteReservoir.integrable_increment line 76
8. lemma OAI.DilutedSpinGlass.ConcreteReservoir.low_averaged_increment line 91
9. lemma OAI.DilutedSpinGlass.ConcreteReservoir.uniform_increment line 105
10. def OAI.DilutedSpinGlass.HeterogeneousMarks.rootExternalTreeScore line 132

    Source documentation

    A fresh independent insertion, retaining every original mark in z. The arguments old and new are intentionally distinct.

    noncomputable def rootExternalTreeScore (S : PrescribedTree L) (a : S.Leaf)
        (T : KernelTower Ω L) (Q : (i : I) → Fin L → FiniteLaw (A i)) (m : Fin L → ℝ)
        (base : RootPath Y M → (k : ℕ) → RootPath X k → FinitePath Ω L → ℝ)
        (old new E : (i : I) → FinitePath Ω L → FinitePath (A i) L → ℝ)
        (f : (S.Leaf → FinitePath Ω L) → ℝ) (z : FullRootState Y X I M) (i : I) : ℝ :=
    …

    Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.RootPath, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.FullRootState

11. def OAI.DilutedSpinGlass.HeterogeneousMarks.rootExternalCoefficient line 139
12. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.measurable_rootExternalTreeScore line 146
13. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.measurable_rootExternalCoefficient line 163
14. def OAI.DilutedSpinGlass.HeterogeneousMarks.externalAverage line 189
15. def OAI.DilutedSpinGlass.HeterogeneousMarks.externalCoefficientAverage line 193
16. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.integrable_rootExternalTreeScore line 204
17. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.integrable_rootExternalCoefficient line 216
18. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.integrable_rootPair_square line 250
19. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.integrable_rootPair_history line 259
20. theorem OAI.DilutedSpinGlass.HeterogeneousMarks.root_model_decorrelation_bound line 271

    Source documentation

    Nonnegative three-copy control for the actual random-reservoir root law. No integrability side conditions or covariance estimates are assumed.

    theorem root_model_decorrelation_bound (hd : d < L) (hab : splitDepth S a b = d)
        (v : S.Internal) (hav : freshSplitDepth S v a = d) (hbv : freshSplitDepth S v b = d)
        (huniq : ∀ c, splitDepth S a c = d → c = b)
        (hm : Monotone m) (hp : ∀ j, 0 ≤ m j) (hend : m (Fin.last L) = 1) :
        (-gamma S m v)*(∫ z, rootConditionalEnergy T Q (fun j => m j.succ) base old d V z ∂μ) ≤
          (m ⟨d+1,by omega⟩-m ⟨d,by omega⟩) +
          pairRootCovariance μ (rootAlphabet (Ω := Ω) (A := A)) L d N
    …

    Mentions: OAI.DilutedSpinGlass.HeterogeneousMarks.rootConditionalEnergy, OAI.DilutedSpinGlass.HeterogeneousMarks.rootAlphabet