OAI/Probability/DilutedSpin/MatrixEnergy.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DilutedSpinGlass.PrescribedTree.grid_strictMono line 16
2. lemma OAI.DilutedSpinGlass.PrescribedTree.grid_nonneg line 22
3. lemma OAI.DilutedSpinGlass.PrescribedTree.grid_last line 26
4. theorem OAI.DilutedSpinGlass.PrescribedTree.pair_energy_test_bound line 31

   Source documentation

   The old test may be the physical overlap, rather than the projected one. Its replacement costs precisely its L2 projection error.

   theorem pair_energy_test_bound (n d : ℕ) (hd : d < n) (K : KernelTower Ω n)
       (m : Fin (n+1) → ℝ) (hm : Monotone m) (hp : ∀ j, 0 ≤ m j)
       (hend : m (Fin.last n) = 1) (S : PrescribedTree n) (x y : S.Leaf) (v : S.Internal)
       (hxy : splitDepth S x y = d) (hxv : freshSplitDepth S v x = d) (hyv : freshSplitDepth S v y = d)
       (X : FinitePath Ω n → Fin N → ℝ) (hX : ∀ z i, |X z i| ≤ 1)
       (hOld : ∀ z, splitDepth S x z = d → ∀ w : Sample Ω S, X (S.pathAt z w) = X (S.pathAt y w))
       (f : Sample Ω S → ℝ) :
       (-gamma S m v)*KernelTower.prefixEnergyAt n K d X ≤
         (m ⟨d+1,by omega⟩-m ⟨d,by omega⟩) +
         pairObservableHistory K m S x d (fun z w => FiniteLaw.dot (X z) (X w)) f +
         pairHistoryMass S m x * (S.sampleLaw K).l2
           (fun z => FiniteLaw.dot (X (S.pathAt x z)) (X (S.pathAt y z))-f z) := by
   …

   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, OAI.DilutedSpinGlass.PrescribedTree.pairObservableHistory, OAI.DilutedSpinGlass.FiniteLaw.dot, OAI.DilutedSpinGlass.PrescribedTree.pairHistoryMass

5. lemma OAI.DilutedSpinGlass.PrescribedTree.signed_approximation line 66
6. theorem OAI.DilutedSpinGlass.PrescribedTree.matrix_energy_pointwise line 81

   Source documentation

   Pointwise-in-the-root crux of the shifted-shape induction. The first term is SIGNED (not the expectation of its absolute value), so the physical perturbation identity can be used after root averaging. Every error is an actual single-copy L2 error and has the literal protected-history charge.

   theorem matrix_energy_pointwise (hL : 0 < L) (Q : Finset ℕ)
       (T S : PrescribedTree L) (q : C → T.Leaf) (hq : Function.Bijective q)
       (hS : branchingCount S (· ∈ Q) = 0) (K : KernelTower Ω L)
       (a c : C) (hac : a ≠ c) (cs : List C) (hcs : cs.Nodup)
       (hdis : ∀ d ∈ cs, d ∉ 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 : FinitePath Ω L → Fin N → ℝ) (hX : ∀ z i, |X z i| ≤ 1)
       (hOld : ∀ z, splitDepth S x z = d → ∀ w : Sample Ω S, X (S.pathAt z w) = X (S.pathAt y w))
       (A : (C → FinitePath Ω L) → ℝ) (f : Sample Ω S → ℝ) (hf : ∀ z, |f z| ≤ 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, OAI.DilutedSpinGlass.PrescribedTree.Sample

7. lemma OAI.DilutedSpinGlass.PrescribedTree.complete_list_nodup line 164
8. lemma OAI.DilutedSpinGlass.PrescribedTree.complete_list_union line 174
9. lemma OAI.DilutedSpinGlass.PrescribedTree.kappa_pair_quotient line 180
10. theorem OAI.DilutedSpinGlass.PrescribedTree.matrixHistory_one_div line 195

    Source documentation

    Exact centering coefficient of an actual matrix-observable history. The normalizer uses the protected PAIR, so one factor -delta remains.

    theorem matrixHistory_one_div (T : PrescribedTree n) (q : C → T.Leaf)
        (hq : Function.Bijective q) (K : KernelTower Ω n) (m : Fin (n+1) → ℝ)
        (hm : StrictMono m) (hp : ∀ j, 0 ≤ m j) (hend : m (Fin.last n) = 1)
        (a c : C) (hac : a ≠ c) (cs : List C) (hcs : cs.Nodup)
        (hdis : ∀ d ∈ cs, d ∉ insert c ({a} : Finset C))
        (hfull : insert c ({a} : Finset C) ∪ cs.toFinset = Finset.univ)
        (S : PrescribedTree n) (x : S.Leaf) (A : (C → FinitePath Ω n) → ℝ)
        (d : ℕ) (hd : d < n) (hqd : splitDepth T (q a) (q c) = d) :
        weightedMatrixHistory T q
          (fun D pos g => (D.sampleLaw K).expect (fun z => g z*A (fun b => D.pathAt (pos b) z)))
          m (c::cs) S (Finset.univ.erase x) id (fun _ => x) (fun _ => 1) /
          (partialKappa T m (Finset.univ.image q) / partialKappa T m ((insert c ({a} : Finset C)).image q)) =
    …

    Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.splitDepth, OAI.DilutedSpinGlass.PrescribedTree.weightedMatrixHistory, OAI.DilutedSpinGlass.PrescribedTree.partialKappa