OAI/Probability/DilutedSpin/MatrixRoot.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DilutedSpinGlass.PrescribedTree.matrixObservableHistory line 13
  2. def OAI.DilutedSpinGlass.PrescribedTree.matrixProjectionError line 20
  3. def OAI.DilutedSpinGlass.PrescribedTree.oldProjectionError line 26
  4. def OAI.DilutedSpinGlass.PrescribedTree.shiftedCharge line 30
  5. def OAI.DilutedSpinGlass.PrescribedTree.matrixRootCovariance line 42
  6. theorem OAI.DilutedSpinGlass.PrescribedTree.root_matrix_energy line 53

    Source documentation

    The full shifted-matrix/three-copy estimate after root averaging. The only analytic errors are actual target and old single-copy L2 projection errors. The prescribed-tree identity appears as ONE centered root covariance, not any stronger conditional or absolute pointwise concentration claim.

    theorem root_matrix_energy {Z : Type} [MeasurableSpace Z] (μ : Measure Z)
    [IsProbabilityMeasure μ] (Ω : Z → Type) [∀ z, Fintype (Ω z)]
    (hL : 0 < L) (Q : Finset ℕ) (T S : PrescribedTree L)
    (q : C → T.Leaf) (hq : Function.Bijective q) (hS : branchingCount S (· ∈ Q) = 0)
    (K : (z : Z) → KernelTower (Ω z) L)
    (a c : C) (hac : a ≠ c) (cs : List C) (hcs : cs.Nodup)
    (hdis : ∀ b ∈ cs, b ∉ insert c ({a} : Finset C))
    (hfull : insert c ({a} : Finset C) ∪ cs.toFinset = Finset.univ)
    (x y : S.Leaf) (v : S.Internal) (d : ℕ) (hd : d < L)
    (hqd : splitDepth T (q a) (q c) = d) (hxy : splitDepth S x y = d)
    (hxv : freshSplitDepth S v x = d) (hyv : freshSplitDepth S v y = d)
    (X : (z : Z) → FinitePath (Ω z) L → Fin N → ℝ) (hX : ∀ z w i, |X z w i| ≤ 1)
…

    Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.PrescribedTree.branchingCount, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.PrescribedTree.splitDepth, OAI.DilutedSpinGlass.PrescribedTree.freshSplitDepth, OAI.DilutedSpinGlass.FinitePath