ConditionalScheduledMean.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

def OAI.DilutedSpinGlass.ReducedTopology.conditionalScheduledMean line 14
Source documentation
The scheduled conditional mean on a literal full path, evaluated after e transitions. Before the first branching this is the usual conditional expectation; no independently sampled prefix occurs in this definition.
```
noncomputable def conditionalScheduledMean : (H d e : ℕ) →
    (S : ReducedTopology) → (S.Vertex → ℕ) → KernelTower Ω H →
    (FinitePath Ω H → ℝ) → FinitePath Ω H → ℝ
  | 0,_,_,_,_,T,f,_ => PrescribedTree.treeMean .leaf T f
  | H+1,d,0,S,q,T,f,_ => PrescribedTree.treeMean (realize (H+1) d S q) T f
  | H+1,d,e+1,S,q,T,f,x => conditionalScheduledMean H (d+1) e S q (T.2 x.1)
      (fun y => f (x.1,y)) x.2
```
Mentions: OAI.DilutedSpinGlass.ReducedTopology, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.treeMean, OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.ReducedTopology.realize
lemma OAI.DilutedSpinGlass.ReducedTopology.conditionalScheduledMean_zero line 22
lemma OAI.DilutedSpinGlass.ReducedTopology.conditionalScheduledMean_bound line 27
lemma OAI.DilutedSpinGlass.ReducedTopology.conditionalScheduledMean_eq_prefix line 38
Source documentation
Exact agreement with the fixed-terminal-reserve evaluation martingale.
```
lemma conditionalScheduledMean_eq_prefix (n r d : ℕ) (S : ReducedTopology) (q : S.Vertex → ℕ)
    (e : Fin (r+1)) (T : KernelTower Ω (n+r)) (f : FinitePath Ω (n+r) → ℝ)
    (x : FinitePath Ω (n+r)) :
    conditionalScheduledMean (n+r) d e.val S q T f x=scheduledPrefixMean n r d e S q T f x := by
…
```
Mentions: OAI.DilutedSpinGlass.ReducedTopology, OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.ReducedTopology.conditionalScheduledMean, OAI.DilutedSpinGlass.ReducedTopology.scheduledPrefixMean
lemma OAI.DilutedSpinGlass.ReducedTopology.conditionalScheduledMean_eq_tail line 53
Source documentation
Exact tail-projector geometry, with the original prefix retained.
```
lemma conditionalScheduledMean_eq_tail (H p d : ℕ) (S : ReducedTopology)
    (q : S.Vertex → ℕ) (T : KernelTower Ω (H+p)) (f : FinitePath Ω (H+p) → ℝ)
    (x : FinitePath Ω (H+p)) :
    conditionalScheduledMean (H+p) d p S q T f x=
      PrescribedTree.tailMean (realize H (d+p) S q) p T f x := by
…
```
Mentions: OAI.DilutedSpinGlass.ReducedTopology, OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.ReducedTopology.conditionalScheduledMean, OAI.DilutedSpinGlass.PrescribedTree.tailMean, OAI.DilutedSpinGlass.ReducedTopology.realize
def OAI.DilutedSpinGlass.ReducedTopology.conditionalScheduledProduct line 67
Source documentation
Proper-child mean product at an actual evaluation prefix, expressed without a choice of terminal reserve.
```
noncomputable def conditionalScheduledProduct {ι : Type*} [Fintype ι]
    (H d e : ℕ) (C : ι → ReducedTopology) (q : (j : ι) → (C j).Vertex → ℕ)
    (T : KernelTower Ω H) (f : FinitePath Ω H → Fin N → ℝ)
    (x : FinitePath Ω H) (i : Fin N) : ℝ :=
…
```
Mentions: OAI.DilutedSpinGlass.ReducedTopology, OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.ReducedTopology.Vertex, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath
lemma OAI.DilutedSpinGlass.ReducedTopology.conditionalScheduledProduct_bound line 73
lemma OAI.DilutedSpinGlass.ReducedTopology.conditionalScheduledProduct_eq_prefix line 82
lemma OAI.DilutedSpinGlass.ReducedTopology.conditionalScheduledProduct_eq_childSchedule line 92
Source documentation
The simultaneous-schedule projector is literally this conditional proper-child product. This is the bridge between the two continuity costs.
```
lemma conditionalScheduledProduct_eq_childSchedule {ι α : Type} [Fintype ι]
    {L : ℕ} [NeZero L] (H p : ℕ) (C : ι → ReducedTopology)
    (e : (j : ι) → (C j).Vertex → α) (τ : (j : ι) → (C j).Vertex → Equiv.Perm (Fin L))
    (s : (j : ι) → (C j).Vertex → Bool) (Q : α → Fin L)
    (T : KernelTower Ω (H+p)) (f : FinitePath Ω (H+p) → Fin N → ℝ) :
    conditionalScheduledProduct (H+p) 0 p C
      (fun j v => (DepthAverage.shiftPerm (s j v) (τ j v (Q (e j v)))).val) T f=
      childScheduleProjection H p p C e τ s T f Q := by
…
```
Mentions: OAI.DilutedSpinGlass.ReducedTopology, OAI.DilutedSpinGlass.ReducedTopology.Vertex, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.ReducedTopology.conditionalScheduledProduct, OAI.DilutedSpinGlass.DepthAverage.shiftPerm, OAI.DilutedSpinGlass.ReducedTopology.childScheduleProjection
def OAI.DilutedSpinGlass.DepthAverage.insertCoordinate line 122
Source documentation
Put a distinguished evaluation coordinate back into its full parent cube, keeping every other branching coordinate literally unchanged.
```
def insertCoordinate (a : α) (t : Fin L) (rest : {j : α // j≠a} → Fin L) : α → Fin L :=
…
```
lemma OAI.DilutedSpinGlass.DepthAverage.insertCoordinate_self line 126
lemma OAI.DilutedSpinGlass.DepthAverage.insertCoordinate_other line 130
lemma OAI.DilutedSpinGlass.DepthAverage.average_split line 135
lemma OAI.DilutedSpinGlass.DepthAverage.average_split_comm line 142
Source documentation
Fix all child coordinates first, then average the evaluation coordinate.
```
lemma average_split_comm (a : α) (D : (α → Fin L) → Prop) (F : (α → Fin L) → ℝ) :
    average D F=(depthLaw {j : α // j≠a} L).expect (fun rest =>
      (FiniteLaw.uniform : FiniteLaw (Fin L)).expect (fun t =>
        if D (insertCoordinate a t rest) then F (insertCoordinate a t rest) else 0)) := by
…
```
Mentions: OAI.DilutedSpinGlass.DepthAverage.average, OAI.DilutedSpinGlass.DepthAverage.depthLaw, OAI.DilutedSpinGlass.FiniteLaw.uniform, OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.DepthAverage.insertCoordinate
lemma OAI.DilutedSpinGlass.DepthAverage.average_of_slice_le line 151
Source documentation
Uniform fixed-evaluation estimates survive the unused evaluation coordinate with no extra L factor.
```
lemma average_of_slice_le (a : α) (D : (α → Fin L) → Prop) (F : (α → Fin L) → ℝ) (c : ℝ)
    (h : ∀ t : Fin L, average (fun rest => D (insertCoordinate a t rest))
      (fun rest => F (insertCoordinate a t rest))≤c) : average D F≤c := by
…
```
Mentions: OAI.DilutedSpinGlass.DepthAverage.average, OAI.DilutedSpinGlass.DepthAverage.insertCoordinate

lemma OAI.DilutedSpinGlass.DepthAverage.sum_zeroExtension line 160

Source documentation

Sum of a literal zero-extended prefix family.

lemma sum_zeroExtension {r : ℕ} (hr : r≤L) (F : Fin r → ℝ) :
    (∑ t : Fin L, if h : t.val<r then F ⟨t.val,h⟩ else 0)=∑ e : Fin r, F e := by
…

lemma OAI.DilutedSpinGlass.DepthAverage.uniform_zeroExtension line 176