OAI/Probability/DilutedSpin/FiniteLogExpansion.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DilutedSpinGlass.PrescribedTree.leafProduct_single line 11
2. theorem OAI.DilutedSpinGlass.PrescribedTree.leafProduct_cast line 20
3. theorem OAI.DilutedSpinGlass.PrescribedTree.leafProduct_grow line 30

   Source documentation

   Exactly one terminal factor is added by growth, and its ancestry is the new path, not a path chosen by equality of sample values.

   theorem leafProduct_grow {n : ℕ} (S : PrescribedTree n) (v : Internal S)
       (f : FinitePath Ω n → ℝ) (x : Sample Ω (grow S v)) :
       leafProduct (grow S v) f x = leafProduct S f (oldSample S v x) * f (newPath S v x) := by
   …

   Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Internal, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.Sample, OAI.DilutedSpinGlass.PrescribedTree.grow, OAI.DilutedSpinGlass.PrescribedTree.leafProduct, OAI.DilutedSpinGlass.PrescribedTree.oldSample, OAI.DilutedSpinGlass.PrescribedTree.newPath

4. def OAI.DilutedSpinGlass.PrescribedTree.qMoment line 93

   Source documentation

   Terminal moment of a genuine prescribed tree, then expectation over Q.

   noncomputable def qMoment {n : ℕ} (m : Fin (n+1) → ℝ) (T : KernelTower Ω n)
       (D : FinitePath Ω n → ℝ) (k : ℕ) (S : PrescribedTree n) : ℝ :=
   …

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

5. theorem OAI.DilutedSpinGlass.PrescribedTree.abs_leafProduct_le_one line 98
6. theorem OAI.DilutedSpinGlass.PrescribedTree.abs_qMoment_le_one line 104
7. theorem OAI.DilutedSpinGlass.PrescribedTree.extensionIterate_eq_qMoment line 114

   Source documentation

   Exact coefficients of all genuine fresh growth histories. Normalizing at successive tree sizes produces the rising factorial, with no guessed law.

   theorem extensionIterate_eq_qMoment {n : ℕ} (m : Fin (n+1) → ℝ)
       (hnz : ∀ j : Fin n, m j.succ ≠ 0) (T : KernelTower Ω n)
       (D : FinitePath Ω n → ℝ) (k : ℕ) (S : PrescribedTree n) :
       extensionIterate T m D k S (leafProduct S D) 0 =
         (-1:ℝ)^k * ((leaves S).ascFactorial k:ℝ) * qMoment m T D k S := by
   …

   Mentions: OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.extensionIterate, OAI.DilutedSpinGlass.PrescribedTree.leafProduct, OAI.DilutedSpinGlass.PrescribedTree.leaves, OAI.DilutedSpinGlass.PrescribedTree.qMoment

8. theorem OAI.DilutedSpinGlass.FiniteLaw.analyticAt_expect line 149
9. theorem OAI.DilutedSpinGlass.FiniteLaw.analyticAt_logMean line 156
10. theorem OAI.DilutedSpinGlass.KernelTower.analyticAt_backwardLog line 167
11. def OAI.DilutedSpinGlass.PrescribedTree.logInsertion line 183
12. def OAI.DilutedSpinGlass.PrescribedTree.logJet line 187
13. theorem OAI.DilutedSpinGlass.PrescribedTree.fullyProtected_single line 192
14. theorem OAI.DilutedSpinGlass.PrescribedTree.hasDerivAt_logJet line 207
15. theorem OAI.DilutedSpinGlass.PrescribedTree.insertion_pos line 224
16. theorem OAI.DilutedSpinGlass.PrescribedTree.iteratedDeriv_logInsertion line 232
17. theorem OAI.DilutedSpinGlass.PrescribedTree.logInsertion_coefficient line 248
18. theorem OAI.DilutedSpinGlass.PrescribedTree.logInsertion_zero line 268
19. theorem OAI.DilutedSpinGlass.PrescribedTree.logInsertion_coefficient_bound line 274
20. theorem OAI.DilutedSpinGlass.PrescribedTree.analyticAt_logInsertion line 289
21. theorem OAI.DilutedSpinGlass.PrescribedTree.hasSum_logInsertion line 299

    Source documentation

    The positive Q tree expansion of the nonlinear power means, valid on the whole physical |t|<1 disk, not merely its unspecified Taylor neighborhood.

    theorem hasSum_logInsertion {n : ℕ} (T : KernelTower Ω n)
        (m : Fin (n+1) → ℝ) (hm : Monotone m) (hpos : ∀ j, 0 ≤ m j)
        (hnz : ∀ j : Fin n, m j.succ ≠ 0) (hroot : m 0 = 0) (hend : m (Fin.last n) = 1)
        (D : FinitePath Ω n → ℝ) (hD : ∀ y, |D y| ≤ 1) {t : ℝ} (ht : |t| < 1) :
        HasSum (fun k => (-1:ℝ)^k / (k+1) * qMoment m T D k (single n) * t^(k+1))
          (logInsertion T m D t) := by
    …

    Mentions: OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.qMoment, OAI.DilutedSpinGlass.PrescribedTree.single, OAI.DilutedSpinGlass.PrescribedTree.logInsertion

22. theorem OAI.DilutedSpinGlass.PrescribedTree.logInsertion_term_bound line 336
23. theorem OAI.DilutedSpinGlass.PrescribedTree.logInsertion_tail_bound line 352
24. theorem OAI.DilutedSpinGlass.ReducedTopology.exists_realize line 398

    Source documentation

    Suppression of unary vertices loses neither the leveled tree nor labels.

    theorem exists_realize {r : ℕ} (T : PrescribedTree r) (d : ℕ) :
        ∃ (S : ReducedTopology) (q : S.Vertex → ℕ),
          Admissible S q d (d+r) ∧ realize r d S q=T := by
    …

    Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.ReducedTopology, OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.ReducedTopology.Admissible, OAI.DilutedSpinGlass.ReducedTopology.realize

25. theorem OAI.DilutedSpinGlass.ReducedTopology.exists_bounded_realize line 435

    Source documentation

    For bounded leaf number there are finitely many possible reduced shapes.

    theorem exists_bounded_realize {r : ℕ} (T : PrescribedTree r) (K : ℕ)
        (hK : T.leaves≤K) :
        ∃ (S : ReducedTopology), S∈boundedTopologies K ∧
          ∃ q : S.Vertex → Fin r,
            Admissible S (fun v => q v) 0 r ∧ realize r 0 S (fun v => q v)=T := by
    …

    Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.ReducedTopology, OAI.DilutedSpinGlass.ReducedTopology.boundedTopologies, OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.ReducedTopology.Admissible, OAI.DilutedSpinGlass.ReducedTopology.realize