MatrixTriple.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

def OAI.DilutedSpinGlass.KernelTower.halfTripleDifferenceAt line 12
Source documentation
The actual half squared three-copy contraction difference. Unlike covariance energy this retains the positive conditional-mean contribution.
```
noncomputable def halfTripleDifferenceAt (n : ℕ) (T : KernelTower Ω n) (d : ℕ)
    (X : FinitePath Ω n → Fin N → ℝ) : ℝ :=
…
```
Mentions: OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath

theorem OAI.DilutedSpinGlass.PrescribedTree.general_three_copy_bound_at line 26

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_three_copy_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.halfTripleDifferenceAt 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.halfTripleDifferenceAt

theorem OAI.DilutedSpinGlass.PrescribedTree.pair_three_copy_test_bound line 82

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_three_copy_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.halfTripleDifferenceAt 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
…

theorem OAI.DilutedSpinGlass.PrescribedTree.matrix_three_copy_pointwise line 121

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_three_copy_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

def OAI.DilutedSpinGlass.PrescribedTree.branchExcess line 205
Source documentation
Higher-degree factors, after removing the one grid increment per branching vertex.
```
noncomputable def branchExcess : {n : ℕ} → PrescribedTree n → ℕ
  | 0, .leaf => 0
  | _+1, .node k C => (k:ℕ)-2 + ∑ i, branchExcess (C i)
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree
lemma OAI.DilutedSpinGlass.PrescribedTree.branchProduct_lower line 209
lemma OAI.DilutedSpinGlass.PrescribedTree.branchProduct_lower_pos line 229
lemma OAI.DilutedSpinGlass.PrescribedTree.leaf_nonempty line 245
lemma OAI.DilutedSpinGlass.PrescribedTree.childRefs_univ line 252
lemma OAI.DilutedSpinGlass.PrescribedTree.partialKappa_univ_node line 259
def OAI.DilutedSpinGlass.PrescribedTree.BranchRegular line 275
Source documentation
Every vertex with at least three children has its higher-degree reference factors bounded away from zero. Binary vertices need only the grid increment.
```
noncomputable def BranchRegular : {n : ℕ} → PrescribedTree n → (Fin (n+1) → ℝ) → ℝ → Prop
  | 0, .leaf, _, _ => True
  | _+1, .node k C, m, η => (2 < (k:ℕ) → η ≤ m 1) ∧
      ∀ i, BranchRegular (C i) (fun j => m j.succ) η
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree
lemma OAI.DilutedSpinGlass.PrescribedTree.branchProduct_lower_regular line 280
theorem OAI.DilutedSpinGlass.PrescribedTree.partialKappa_grid_lower line 300