MarkerVariance.lean`

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

def OAI.DilutedSpinGlass.PrescribedTree.forkOverlap line 12
Source documentation
The complete overlap in one of two conditionally independent descendants of an actually sampled stem.
```
noncomputable def forkOverlap (A : PrescribedTree n) : (r : ℕ) →
    (FinitePath Ω (n+1+r) → Fin N → ℝ) → Fin 2 → Sample Ω (stem (doubled A) r) → ℝ
  | 0, V, j, w => treeOverlap A (fun y => V ((w j).1,y)) (w j).2
  | r+1, V, j, w => forkOverlap A r (fun y => V ((w 0).1,y)) j (w 0).2

omit [Fintype Ω] in
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.Sample, OAI.DilutedSpinGlass.PrescribedTree.stem, OAI.DilutedSpinGlass.PrescribedTree.doubled, OAI.DilutedSpinGlass.PrescribedTree.treeOverlap
lemma OAI.DilutedSpinGlass.PrescribedTree.forkOverlap_paths line 18
def OAI.DilutedSpinGlass.PrescribedTree.forkPairMean line 35
def OAI.DilutedSpinGlass.PrescribedTree.unarySquareMean line 39
lemma OAI.DilutedSpinGlass.PrescribedTree.forkPairMean_zero line 43
lemma OAI.DilutedSpinGlass.PrescribedTree.forkPairMean_succ line 57
lemma OAI.DilutedSpinGlass.PrescribedTree.unarySquareMean_succ line 64
lemma OAI.DilutedSpinGlass.PrescribedTree.unarySquareMean_zero line 74
lemma OAI.DilutedSpinGlass.PrescribedTree.marker_conditional_variance_zero line 86
theorem OAI.DilutedSpinGlass.PrescribedTree.marker_conditional_variance_le line 104
Source documentation
Whole-shape conditional variance is controlled by the whole-shape covariance energy. There is no missing projection or independence premise.
```
theorem marker_conditional_variance_le (A : PrescribedTree n) (r : ℕ)
    (K : KernelTower Ω (n+1+r)) (V : FinitePath Ω (n+1+r) → Fin N → ℝ) :
    unarySquareMean A r K V - forkPairMean A r K V ≤ Real.sqrt (shapeEnergyAt A r K V) := by
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.unarySquareMean, OAI.DilutedSpinGlass.PrescribedTree.forkPairMean, OAI.DilutedSpinGlass.PrescribedTree.shapeEnergyAt
lemma OAI.DilutedSpinGlass.PrescribedTree.markerOld_overlap line 115
lemma OAI.DilutedSpinGlass.PrescribedTree.markerFresh_overlap line 127