OAI/Probability/DilutedSpin/ExternalTaylor.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DilutedSpinGlass.HeterogeneousMarks.rootPairObservable line 16
2. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.measurable_rootPairObservable line 35
3. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.rootPairObservable_bound line 52
4. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.integrable_rootPairObservable line 58
5. theorem OAI.DilutedSpinGlass.PrescribedTree.measurable_anchorIterate_zero line 79

   Source documentation

   Measurability of every coefficient of the actual finite extension recursion, from measurable old-tree expectations.

   theorem measurable_anchorIterate_zero (T : Z → KernelTower Ω n)
       (m : Fin (n+1) → ℝ) (hm : ∀ j : Fin n, m j.succ ≠ 0)
       (hT : ∀ (S : PrescribedTree n) (G : S.Sample Ω → ℝ),
         Measurable (fun z => (S.sampleLaw (T z)).expect G))
       (D : FinitePath Ω n → ℝ) {ι : Type} [DecidableEq ι]
       (k : ℕ) (S : PrescribedTree n) (A : Finset ι)
       (U : ι → S.Sample Ω → FinitePath Ω n) (G : S.Sample Ω → ℝ) :
       Measurable (fun z => anchorIterate (T z) m D k S A U G 0) := by
   …

   Mentions: OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.anchorIterate

6. def OAI.DilutedSpinGlass.HeterogeneousMarks.externalCoefficient line 102
7. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.measurable_externalTreeScore line 116
8. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.measurable_externalCoefficient line 131
9. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.abs_externalTreeScore_le line 150
10. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.externalCoefficient_bound line 184
11. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.externalTreeScore_sub_le line 198
12. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.externalTreeScore_taylor_bound line 215