ScheduledEvaluationContinuity.lean`

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

def OAI.DilutedSpinGlass.ReducedTopology.scheduledPrefixMean line 14
Source documentation
Conditional scheduled-tree mean after a genuine sampled prefix. The terminal reserve n is held fixed and the evaluation depth ranges over the first r transitions. No unobserved ancestral variable is resampled.
```
noncomputable def scheduledPrefixMean (n : ℕ) : (r d : ℕ) → Fin (r+1) →
    (S : ReducedTopology) → (S.Vertex → ℕ) → KernelTower Ω (n+r) →
    (FinitePath Ω (n+r) → ℝ) → FinitePath Ω (n+r) → ℝ
  | 0,d,_,S,q,T,f,_ => PrescribedTree.treeMean (realize n d S q) T f
  | r+1,d,e,S,q,T,f,x => Fin.cases
      (PrescribedTree.treeMean (realize (n+r+1) d S q) T f)
      (fun e => scheduledPrefixMean n r (d+1) e S q (T.2 x.1) (fun y => f (x.1,y)) x.2) e
```
Mentions: OAI.DilutedSpinGlass.ReducedTopology, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.PrescribedTree.treeMean, OAI.DilutedSpinGlass.ReducedTopology.realize
lemma OAI.DilutedSpinGlass.ReducedTopology.scheduledPrefixMean_zero line 22
lemma OAI.DilutedSpinGlass.ReducedTopology.scheduledPrefixMean_eq_stemMeanAt line 30
Source documentation
Before the first child branching the literal scheduled conditional mean is exactly the martingale used in the energy theorem. All later assigned depths stay fixed in this identity.
```
lemma scheduledPrefixMean_eq_stemMeanAt (n r d : ℕ) (S : ReducedTopology)
    (q : S.Vertex → ℕ) (hq : ∀ v, d+r≤q v) (e : Fin (r+1))
    (T : KernelTower Ω (n+r)) (f : FinitePath Ω (n+r) → ℝ) (x : FinitePath Ω (n+r)) :
    scheduledPrefixMean n r d e S q T f x=
      PrescribedTree.stemMeanAt (realize n (d+r) S q) r e T f x := by
…
```
Mentions: OAI.DilutedSpinGlass.ReducedTopology, OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.ReducedTopology.scheduledPrefixMean, OAI.DilutedSpinGlass.PrescribedTree.stemMeanAt, OAI.DilutedSpinGlass.ReducedTopology.realize
def OAI.DilutedSpinGlass.ReducedTopology.scheduledProductMean line 46
Source documentation
Ranged proper-child conditional product in the actual scheduled shape.
```
noncomputable def scheduledProductMean {ι : Type*} [Fintype ι]
    (n r d : ℕ) (C : ι → ReducedTopology) (q : (j : ι) → (C j).Vertex → ℕ)
    (e : Fin (r+1)) (T : KernelTower Ω (n+r)) (f : FinitePath Ω (n+r) → Fin N → ℝ)
    (x : FinitePath Ω (n+r)) (i : Fin N) : ℝ :=
…
```
Mentions: OAI.DilutedSpinGlass.ReducedTopology, OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.ReducedTopology.Vertex, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath
lemma OAI.DilutedSpinGlass.ReducedTopology.scheduledProductMean_eq line 52
theorem OAI.DilutedSpinGlass.ReducedTopology.scheduled_target_evaluation_cost_le line 67
Source documentation
The evaluation component of h_N on the exact scheduled proper-child family, with later branching depths fixed and arbitrary allowed evaluation subsets. Targets and anchors may vary with the evaluation coordinate.
```
theorem scheduled_target_evaluation_cost_le {ι : Type*} [Fintype ι]
    (n r d L : ℕ) (C : ι → ReducedTopology) (q : (j : ι) → (C j).Vertex → ℕ)
    (hq : ∀ j v, d+r≤q j v) (U : Finset (Fin r))
    (T : KernelTower Ω (n+r)) (f : FinitePath Ω (n+r) → Fin N → ℝ) (hf : ∀ x i, |f x i|≤1)
    (Target : Fin r → PrescribedTree (n+r)) (a b : (e : Fin r) → (Target e).Leaf) :
    (∑ e ∈ U, PrescribedTree.targetContractionChangeSq (Target e) T (a e) (b e)
      (scheduledProductMean n r d C q e.succ T f)
      (scheduledProductMean n r d C q e.castSucc T f))/(L:ℝ) ≤
      4*(Fintype.card ι:ℝ)^2/(L:ℝ) := by
…
```
Mentions: OAI.DilutedSpinGlass.ReducedTopology, OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.ReducedTopology.Vertex, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.ReducedTopology.Leaf, OAI.DilutedSpinGlass.PrescribedTree.targetContractionChangeSq, OAI.DilutedSpinGlass.ReducedTopology.scheduledProductMean