OAI/Probability/DilutedSpin/SingletonRoot.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DilutedSpinGlass.FiniteLaw.abs_expect_mul_le_l2 line 14
2. lemma OAI.DilutedSpinGlass.PrescribedTree.grow_l2 line 33
3. lemma OAI.DilutedSpinGlass.PrescribedTree.pairObservableHistory_sub_test line 39
4. theorem OAI.DilutedSpinGlass.PrescribedTree.pairObservableHistory_l2 line 68

   Source documentation

   Changing the old test has its original L2 cost, not a sup norm cost; fresh branches preserve its entire old marginal.

   theorem pairObservableHistory_l2 (K : KernelTower Ω n) (m : Fin (n+1) → ℝ)
       (S : PrescribedTree n) (a : S.Leaf) (d : ℕ)
       (R : FinitePath Ω n → FinitePath Ω n → ℝ) (f : Sample Ω S → ℝ)
       (hR : ∀ x y, |R x y| ≤ 1) :
       |pairObservableHistory K m S a d R f| ≤ pairHistoryMass S m a*(S.sampleLaw K).l2 f := by
   …

   Mentions: OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.Sample, OAI.DilutedSpinGlass.PrescribedTree.pairObservableHistory, OAI.DilutedSpinGlass.PrescribedTree.pairHistoryMass

5. theorem OAI.DilutedSpinGlass.PrescribedTree.general_decorrelation_bound_at line 111

   Source documentation

   The nonnegative three-copy argument on an ARBITRARY old tree. Only the geometric grouping of eligible paths is needed; all old paths and the test are retained. This applies to the projected means of multi-leaf shapes.

   theorem general_decorrelation_bound_at (n d : ℕ) (hd : d < n) (T : KernelTower Ω n)
       (m : Fin (n+1) → ℝ) (hm : Monotone m) (hp : ∀ j, 0 ≤ m j)
       (hend : m (Fin.last n) = 1)
       (S : PrescribedTree n) (a b : S.Leaf) (v : S.Internal)
       (hab : splitDepth S a b = d)
       (hav : freshSplitDepth S v a = d) (hbv : freshSplitDepth S v b = d)
       (X : FinitePath Ω n → Fin N → ℝ)
       (hOld : ∀ c, splitDepth S a c = d → ∀ x : Sample Ω S,
         X (S.pathAt c x) = X (S.pathAt b x)) :
       (-gamma S m v)*KernelTower.prefixEnergyAt n T d X ≤
         (m ⟨d+1,by omega⟩-m ⟨d,by omega⟩) *
           (S.sampleLaw T).expect (fun x =>
   …

   Mentions: OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.splitDepth, OAI.DilutedSpinGlass.PrescribedTree.freshSplitDepth, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.Sample, OAI.DilutedSpinGlass.PrescribedTree.gamma, OAI.DilutedSpinGlass.KernelTower.prefixEnergyAt

6. lemma OAI.DilutedSpinGlass.FiniteLaw.abs_dot_le_one line 166
7. def OAI.DilutedSpinGlass.PrescribedTree.rootPairMean line 190
8. def OAI.DilutedSpinGlass.PrescribedTree.rootPairSecond line 195
9. def OAI.DilutedSpinGlass.PrescribedTree.rootPairCovariance line 200
10. lemma OAI.DilutedSpinGlass.PrescribedTree.rootPairCovariance_center line 210
11. theorem OAI.DilutedSpinGlass.PrescribedTree.singleton_root_bound line 237

    Source documentation

    Disorder-averaged singleton inequality with the ACTUAL signed-history covariance. Root variables and all reservoir alphabets may depend on z.

    theorem singleton_root_bound
        (hm : Monotone m) (hp : ∀ j, 0 ≤ m j) (hend : m (Fin.last (h+1+d)) = 1)
        (hX : ∀ z x i, |X z x i| ≤ 1)
        (hE : Integrable (fun z => KernelTower.prefixCovarianceEnergy h d (T z) (X z)) μ)
        (hA : Integrable (fun z => ((fork h 2 d).sampleLaw (T z)).expect (fun x =>
          FiniteLaw.dot (X z ((fork h 2 d).pathAt (forkLeaf h 2 d 0) x))
            (X z ((fork h 2 d).pathAt (forkLeaf h 2 d 1) x))^2)) μ)
        (hH : Integrable (fun z => pairObservableHistory (T z) m (fork h 2 d) (forkLeaf h 2 d 0) d
          (fun x y => FiniteLaw.dot (X z x) (X z y))
          (fun x => FiniteLaw.dot (X z ((fork h 2 d).pathAt (forkLeaf h 2 d 0) x))
            (X z ((fork h 2 d).pathAt (forkLeaf h 2 d 1) x)))) μ) :
        (2*m ⟨d+1,by omega⟩-m ⟨d,by omega⟩) *
    …

    Mentions: OAI.DilutedSpinGlass.KernelTower.prefixCovarianceEnergy, OAI.DilutedSpinGlass.PrescribedTree.fork, OAI.DilutedSpinGlass.PrescribedTree.sampleLaw, OAI.DilutedSpinGlass.FiniteLaw.dot, OAI.DilutedSpinGlass.PrescribedTree.pathAt, OAI.DilutedSpinGlass.PrescribedTree.forkLeaf, OAI.DilutedSpinGlass.PrescribedTree.pairObservableHistory

12. def OAI.DilutedSpinGlass.HeterogeneousMarks.rootTreeMean line 286
13. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.rootTreeMean_eq_selected line 298
14. def OAI.DilutedSpinGlass.HeterogeneousMarks.oldTreeAverage line 314
15. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.measurable_rootTreeMean line 317
16. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.rootTreeMean_bound line 331
17. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.oldTreeAverage_bound line 336
18. def OAI.DilutedSpinGlass.HeterogeneousMarks.parameterError line 357
19. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.selectedParameterFactor_eq line 369
20. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.parameterFactor_log_bound line 378
21. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.parameterError_nonneg line 400
22. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.measurable_parameterError line 404
23. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.parameterError_refresh line 414
24. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.integrable_parameterError line 423