TargetScheduleContinuity.lean`

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.DilutedSpinGlass.DepthAverage.average_expect line 14
lemma OAI.DilutedSpinGlass.DepthAverage.average_mono_on line 27
lemma OAI.DilutedSpinGlass.DepthAverage.average_mul_left line 35
def OAI.DilutedSpinGlass.ReducedTopology.scheduledTailProjection line 52
Source documentation
A branching-schedule projector evaluated on the SAME actual full path. Its initial p coordinates are retained, not independently resampled.
```
noncomputable def scheduledTailProjection (H d p : ℕ) (S : ReducedTopology)
    (q : S.Vertex → Fin L) (T : KernelTower Ω (H+p))
    (f : FinitePath Ω (H+p) → Fin N → ℝ) (x : FinitePath Ω (H+p)) (i : Fin N) : ℝ :=
…
```
Mentions: OAI.DilutedSpinGlass.ReducedTopology, OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath
lemma OAI.DilutedSpinGlass.ReducedTopology.scheduledTailProjection_bound line 58
def OAI.DilutedSpinGlass.ReducedTopology.tailScheduleChange line 64
lemma OAI.DilutedSpinGlass.ReducedTopology.tailScheduleChange_succ line 71
theorem OAI.DilutedSpinGlass.ReducedTopology.averaged_tailScheduleChange_le line 80
Source documentation
Uniform simultaneous schedule continuity after an arbitrary real sampled prefix. In particular p=d gives the physical evaluation-depth geometry.
```
theorem averaged_tailScheduleChange_le (H d p : ℕ) (hheight : d+H=L)
    (S : ReducedTopology) (η : ℝ) (hlarge : 1<η*(L:ℝ)) (s : S.Vertex → Bool)
    (D : (S.Vertex → Fin L) → Prop)
    (hD : ∀ q, D q → Admissible S (fun v => (q v).val) d L ∧ DepthAverage.Regular η q)
    (T : KernelTower Ω (H+p)) (f : FinitePath Ω (H+p) → Fin N → ℝ) (hf : ∀ x i, |f x i|≤1) :
    DepthAverage.average D (tailScheduleChange H d p S s T f) ≤
      (Fintype.card S.Vertex:ℝ)*(∑ v : S.Vertex, (vertexArity S v:ℝ)^2)/(L:ℝ) := by
…
```
Mentions: OAI.DilutedSpinGlass.ReducedTopology, OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.ReducedTopology.Admissible, OAI.DilutedSpinGlass.DepthAverage.Regular, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.DepthAverage.average, OAI.DilutedSpinGlass.ReducedTopology.tailScheduleChange, OAI.DilutedSpinGlass.ReducedTopology.vertexArity
theorem OAI.DilutedSpinGlass.ReducedTopology.averaged_target_schedule_change_le line 110
Source documentation
Full actual target contraction continuity for simultaneous shifts of any subset of branching depths. The target may depend on EVERY schedule coordinate, so no regularity of a union old/target shape is postulated.
```
theorem averaged_target_schedule_change_le (H d p : ℕ) (hheight : d+H=L)
    (S : ReducedTopology) (η : ℝ) (hlarge : 1<η*(L:ℝ)) (s : S.Vertex → Bool)
    (D : (S.Vertex → Fin L) → Prop)
    (hD : ∀ q, D q → Admissible S (fun v => (q v).val) d L ∧ DepthAverage.Regular η q)
    (T : KernelTower Ω (H+p)) (f : FinitePath Ω (H+p) → Fin N → ℝ) (hf : ∀ x i, |f x i|≤1)
    (Target : (S.Vertex → Fin L) → PrescribedTree (H+p))
    (a b : (q : S.Vertex → Fin L) → (Target q).Leaf) :
    DepthAverage.average D (fun q => PrescribedTree.targetContractionChangeSq (Target q) T (a q) (b q)
      (scheduledTailProjection H d p S q T f)
      (scheduledTailProjection H d p S (fun v => DepthAverage.shiftPerm (s v) (q v)) T f)) ≤
      4*((Fintype.card S.Vertex:ℝ)*(∑ v : S.Vertex, (vertexArity S v:ℝ)^2)/(L:ℝ)) := by
…
```
Mentions: OAI.DilutedSpinGlass.ReducedTopology, OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.ReducedTopology.Admissible, OAI.DilutedSpinGlass.DepthAverage.Regular, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.ReducedTopology.Leaf, OAI.DilutedSpinGlass.DepthAverage.average, OAI.DilutedSpinGlass.PrescribedTree.targetContractionChangeSq, OAI.DilutedSpinGlass.ReducedTopology.scheduledTailProjection, OAI.DilutedSpinGlass.DepthAverage.shiftPerm, OAI.DilutedSpinGlass.ReducedTopology.vertexArity