TargetEvaluationContinuity.lean`

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

def OAI.DilutedSpinGlass.PrescribedTree.targetContractionChangeSq line 14
Source documentation
Squared norm of the change of the two-leaf contraction in its actual joint target law, not a product of its marginals.
```
noncomputable def targetContractionChangeSq (S : PrescribedTree n) (T : KernelTower Ω n)
    (a b : S.Leaf) (X Y : FinitePath Ω n → Fin N → ℝ) : ℝ :=
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath
lemma OAI.DilutedSpinGlass.PrescribedTree.targetContractionChangeSq_nonneg line 20
lemma OAI.DilutedSpinGlass.PrescribedTree.targetContractionChangeSq_le line 27
Source documentation
Exact leaf marginalization gives a uniform comparison for any target, even one depending on the evaluation depth and all its branching coordinates.
```
lemma targetContractionChangeSq_le (S : PrescribedTree n) (T : KernelTower Ω n)
    (a b : S.Leaf) (X Y : FinitePath Ω n → Fin N → ℝ)
    (hX : ∀ x i, |X x i|≤1) (hY : ∀ x i, |Y x i|≤1) :
    targetContractionChangeSq S T a b X Y ≤
      4*(KernelTower.law n T).expect (fun x => FiniteLaw.spatialSq (fun i => X x i-Y x i)) := by
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.targetContractionChangeSq, OAI.DilutedSpinGlass.KernelTower.law, OAI.DilutedSpinGlass.FiniteLaw.spatialSq
def OAI.DilutedSpinGlass.PrescribedTree.productStemMeanAt line 41
Source documentation
Actual product of the proper-child conditional means on a single path.
```
noncomputable def productStemMeanAt {ι : Type*} [Fintype ι]
    (C : ι → PrescribedTree n) (r : ℕ) (d : Fin (r+1)) (T : KernelTower Ω (n+r))
    (f : FinitePath Ω (n+r) → Fin N → ℝ) (x : FinitePath Ω (n+r)) (j : Fin N) : ℝ :=
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath
lemma OAI.DilutedSpinGlass.PrescribedTree.productStemMeanAt_bound line 46
lemma OAI.DilutedSpinGlass.PrescribedTree.productStemMeanAt_spatial_increment line 55
theorem OAI.DilutedSpinGlass.PrescribedTree.averaged_target_evaluation_change_le line 65