OAI/Probability/DilutedSpin/SpatialScheduledContinuity.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DilutedSpinGlass.DepthAverage.average_div line 13
2. lemma OAI.DilutedSpinGlass.DepthAverage.average_sum line 21
3. def OAI.DilutedSpinGlass.ReducedTopology.spatialScheduleChange line 40

   Source documentation

   Actual normalized spatial squared norm of the conditional-mean change. Both schedules use the same ancestral kernel and spin function.

   noncomputable def spatialScheduleChange (H d : ℕ) (S : ReducedTopology) (s : S.Vertex → Bool)
       (T : KernelTower Ω H) (f : FinitePath Ω H → Fin N → ℝ) (q : S.Vertex → Fin L) : ℝ :=
   …

   Mentions: OAI.DilutedSpinGlass.ReducedTopology, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.q

4. lemma OAI.DilutedSpinGlass.ReducedTopology.spatialScheduleChange_nonneg line 48
5. theorem OAI.DilutedSpinGlass.ReducedTopology.averaged_spatialScheduleChange_le line 57

   Source documentation

   Full vector-valued branching-depth part of decor:depth-continuity. The constant b*sum(arity²) is independent of N, all transition kernels and the spin function. N=0 obeys the same inequality without an extra hypothesis.

   theorem averaged_spatialScheduleChange_le (H d : ℕ) (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) (f : FinitePath Ω H → Fin N → ℝ) (hf : ∀ x i, |f x i|≤1) :
       DepthAverage.average D (spatialScheduleChange H d 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.spatialScheduleChange, OAI.DilutedSpinGlass.ReducedTopology.vertexArity

6. theorem OAI.DilutedSpinGlass.ReducedTopology.prefix_averaged_spatialScheduleChange_le line 80

   Source documentation

   Uniformity survives the ACTUAL law of any already sampled ancestral prefix; it can even have prefix-dependent finite alphabets.

   theorem prefix_averaged_spatialScheduleChange_le {Z : Type} [Fintype Z] (P : FiniteLaw Z)
       (Ω : Z → Type) [∀ z, Fintype (Ω z)] (H d : ℕ) (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 : (z : Z) → KernelTower (Ω z) H) (f : (z : Z) → FinitePath (Ω z) H → Fin N → ℝ)
       (hf : ∀ z x i, |f z x i|≤1) :
       P.expect (fun z => DepthAverage.average D (spatialScheduleChange H d S s (T z) (f z))) ≤
         (Fintype.card S.Vertex:ℝ)*(∑ v : S.Vertex, (vertexArity S v:ℝ)^2)/(L:ℝ) := by
   …

   Mentions: OAI.DilutedSpinGlass.FiniteLaw, 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.spatialScheduleChange, OAI.DilutedSpinGlass.ReducedTopology.vertexArity

7. theorem OAI.DilutedSpinGlass.ReducedTopology.root_averaged_spatialScheduleChange_le line 99

   Source documentation

   The same estimate after arbitrary probability root averaging. Only ordinary integrability is requested; the bounded error is computed from literal trees, not introduced as an abstract error variable.

   theorem root_averaged_spatialScheduleChange_le {Z : Type} [MeasurableSpace Z]
       (μ : MeasureTheory.Measure Z) [MeasureTheory.IsProbabilityMeasure μ]
       (Ω : Z → Type) [∀ z, Fintype (Ω z)] (H d : ℕ) (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 : (z : Z) → KernelTower (Ω z) H) (f : (z : Z) → FinitePath (Ω z) H → Fin N → ℝ)
       (hf : ∀ z x i, |f z x i|≤1)
       (hI : MeasureTheory.Integrable
         (fun z => DepthAverage.average D (spatialScheduleChange H d S s (T z) (f z))) μ) :
       (∫ z, DepthAverage.average D (spatialScheduleChange H d S s (T z) (f z)) ∂μ) ≤
         (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.spatialScheduleChange, OAI.DilutedSpinGlass.ReducedTopology.vertexArity