MatrixLeafProjection.lean`

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.DilutedSpinGlass.PrescribedTree.spatialProduct_leafProduct line 15
Source documentation
The physical color-indexed spatial product is exactly the product of all actual target leaves whenever colors enumerate those leaves bijectively.
```
lemma spatialProduct_leafProduct (S : PrescribedTree n) (q : I → S.Leaf)
    (hq : Function.Bijective q) (f : FinitePath Ω n → Fin N → ℝ) (z : Sample Ω S) :
    spatialProduct (fun _ : I => f) (fun c => S.pathAt (q c) z) =
      (∑ i, leafProduct S (fun x => f x i) z)/(N:ℝ) := by
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.Sample, OAI.DilutedSpinGlass.PrescribedTree.spatialProduct, OAI.DilutedSpinGlass.PrescribedTree.leafProduct
lemma OAI.DilutedSpinGlass.PrescribedTree.doubledOverlap_bound line 27
lemma OAI.DilutedSpinGlass.PrescribedTree.matrixProjectionError_doubled line 36
Source documentation
Literal target error in the matrix identity, retaining the exact color positions and full all-leaf target overlap.
```
lemma matrixProjectionError_doubled (S : PrescribedTree n) (q : I → (doubled S).Leaf)
    (hq : Function.Bijective q) (T : KernelTower Ω (n+1)) (a c : I) (b : S.Leaf)
    (ha : q a=⟨0,b⟩) (hc : q c=⟨1,b⟩) (f X : FinitePath Ω (n+1) → Fin N → ℝ) :
    matrixProjectionError (doubled S) q T a c (spatialProduct (fun _ : I => f)) X =
      oldProjectionError (doubled S) T ⟨0,b⟩ ⟨1,b⟩ (doubledOverlap S f) X := by
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.PrescribedTree.doubled, OAI.DilutedSpinGlass.PrescribedTree.Leaf, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.matrixProjectionError, OAI.DilutedSpinGlass.PrescribedTree.spatialProduct, OAI.DilutedSpinGlass.PrescribedTree.oldProjectionError, OAI.DilutedSpinGlass.PrescribedTree.doubledOverlap
theorem OAI.DilutedSpinGlass.PrescribedTree.matrixProjectionError_stem_le line 56
Source documentation
Thus the target's own later-first-split projection has the genuine proper-child covariance bound required before making the depth comparison.
```
theorem matrixProjectionError_stem_le (k : ℕ+) (C : Fin k → PrescribedTree n)
    (b : (PrescribedTree.node k C).Leaf) (r : ℕ)
    (q : I → (doubled (stem (.node k C) r)).Leaf) (hq : Function.Bijective q)
    (T : KernelTower Ω (n+1+r+1)) (a c : I)
    (ha : q a=⟨0,stemLeaf (.node k C) r b⟩) (hc : q c=⟨1,stemLeaf (.node k C) r b⟩)
    (f : FinitePath Ω (n+1+r+1) → Fin N → ℝ) (hf : ∀ x i, |f x i|≤1) :
    matrixProjectionError (doubled (stem (.node k C) r)) q T a c
      (spatialProduct (fun _ : I => f))
      (fun x i => tailMean (.node k C) (r+1) T (fun y => f y i) x) ≤
       2*Real.sqrt ((k:ℝ)*∑ i, Real.sqrt (shapeEnergyAt (C i) (r+1) T f)) := by
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Leaf, OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.PrescribedTree.doubled, OAI.DilutedSpinGlass.PrescribedTree.stem, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.PrescribedTree.stemLeaf, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.matrixProjectionError, OAI.DilutedSpinGlass.PrescribedTree.spatialProduct, OAI.DilutedSpinGlass.PrescribedTree.tailMean, OAI.DilutedSpinGlass.PrescribedTree.shapeEnergyAt
theorem OAI.DilutedSpinGlass.PrescribedTree.matrixProjectionError_change line 73
Source documentation
Changing the target's projected means to the old projected means costs their actual coupled L2 difference in the target law, uniformly over extension histories after marginalization.
```
theorem matrixProjectionError_change (S : PrescribedTree n) (q : I → S.Leaf)
    (T : KernelTower Ω n) (a c : I) (A : (I → FinitePath Ω n) → ℝ)
    (X Y : FinitePath Ω n → Fin N → ℝ) :
    matrixProjectionError S q T a c A X ≤ matrixProjectionError S q T a c A Y +
      (S.sampleLaw T).l2 (fun z => FiniteLaw.dot (Y (S.pathAt (q a) z)) (Y (S.pathAt (q c) z))-
        FiniteLaw.dot (X (S.pathAt (q a) z)) (X (S.pathAt (q c) z))) := by
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.matrixProjectionError, OAI.DilutedSpinGlass.FiniteLaw.dot