HeterogeneousProjection.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.DilutedSpinGlass.HeterogeneousMarks.tower_projects line 15
Source documentation
Adjoining an unused physical coordinate preserves every realized mark prior, also when the mark spaces have type-dependent dimensions.
```
theorem tower_projects (π : Ω → Λ) (roots : Fin k → I)
    (T : KernelTower Ω L) (U : KernelTower Λ L) (h : KernelTower.Projects π L T U)
    (Q : (i : I) → Fin L → FiniteLaw (A i)) :
    KernelTower.Projects (fun z : Ω × Row (A := A) roots => (π z.1,z.2)) L
…
```
Mentions: OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.KernelTower.Projects, OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.HeterogeneousMarks.Row
theorem OAI.DilutedSpinGlass.HeterogeneousMarks.physical_pathMap line 28
theorem OAI.DilutedSpinGlass.HeterogeneousMarks.mark_pathMap line 37

theorem OAI.DilutedSpinGlass.HeterogeneousMarks.root_projection line 46

Source documentation

Exact projection through the literal perturbed power-mean root.

theorem root_projection (π : Ω → Λ) (roots : Fin k → I)
    (T : KernelTower Ω L) (U : KernelTower Λ L) (h : KernelTower.Projects π L T U)
    (Q : (i : I) → Fin L → FiniteLaw (A i)) (m : Fin L → ℝ)
    (base : FinitePath Λ L → ℝ)
    (factor : (i : I) → FinitePath Λ L → FinitePath (A i) L → ℝ) :
    root T Q m (fun y => base (KernelTower.pathMap π L y)) roots
      (fun i x y => factor i (KernelTower.pathMap π L x) y) =
    root U Q m base roots factor := by
…

Mentions: OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.KernelTower.Projects, OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.HeterogeneousMarks.root, OAI.DilutedSpinGlass.KernelTower.pathMap

theorem OAI.DilutedSpinGlass.HeterogeneousMarks.root_projection_stability line 63
def OAI.DilutedSpinGlass.PrescribedTree.childEnergy line 91
Source documentation
Covariance energy of one actual child, including its incoming transition. The rest of the tree has not been sampled or conditioned upon.
```
noncomputable def childEnergy {n : ℕ} (C : PrescribedTree n)
    (T : KernelTower Ω (n+1)) (f : FinitePath Ω (n+1) → Fin N → ℝ) : ℝ :=
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath
theorem OAI.DilutedSpinGlass.PrescribedTree.node_projection line 99
Source documentation
Literal child-by-child projection of a prescribed-tree multioverlap. Each factor is a spin product sampled from an actual independent child law. This is the projection error used before signed-history charging.
```
theorem node_projection {n : ℕ} (k : ℕ+) (C : Fin k → PrescribedTree n)
    (T : KernelTower Ω (n+1)) (f : FinitePath Ω (n+1) → Fin N → ℝ)
    (hf : ∀ x v, |f x v| ≤ 1) (B : Fin N → ℝ) (hB : ∀ v, |B v| ≤ 1) :
    ((PrescribedTree.node k C).sampleLaw T).l2 (fun z => FiniteLaw.dot
      (fun v => (PrescribedTree.node k C).leafProduct (fun x => f x v) z -
        (PrescribedTree.node k C).treeMean T (fun x => f x v)) B) ≤
      ∑ i, Real.sqrt (Real.sqrt (childEnergy (C i) T f)) := by
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.sampleLaw, OAI.DilutedSpinGlass.FiniteLaw.dot, OAI.DilutedSpinGlass.PrescribedTree.leafProduct, OAI.DilutedSpinGlass.PrescribedTree.treeMean, OAI.DilutedSpinGlass.PrescribedTree.childEnergy

theorem OAI.DilutedSpinGlass.PrescribedTree.node_projection_independent line 123

Source documentation

The multiplying side is allowed to be an independently sampled complete shape, not merely a deterministic vector. This retains its full joint law.

theorem node_projection_independent {n : ℕ} {Λ : Type*} [Fintype Λ]
    (Q : FiniteLaw Λ) (k : ℕ+) (C : Fin k → PrescribedTree n)
    (T : KernelTower Ω (n+1)) (f : FinitePath Ω (n+1) → Fin N → ℝ)
    (hf : ∀ x v, |f x v| ≤ 1) (B : Λ → Fin N → ℝ) (hB : ∀ z v, |B z v| ≤ 1) :
    (Q.bind (fun _ => (PrescribedTree.node k C).sampleLaw T)).l2 (fun z => FiniteLaw.dot
      (fun v => (PrescribedTree.node k C).leafProduct (fun x => f x v) z.2 -
        (PrescribedTree.node k C).treeMean T (fun x => f x v)) (B z.1)) ≤
      ∑ i, Real.sqrt (Real.sqrt (childEnergy (C i) T f)) := by
…

Mentions: OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.sampleLaw, OAI.DilutedSpinGlass.FiniteLaw.dot, OAI.DilutedSpinGlass.PrescribedTree.leafProduct, OAI.DilutedSpinGlass.PrescribedTree.treeMean, OAI.DilutedSpinGlass.PrescribedTree.childEnergy