OAI/Probability/DilutedSpin/ProjectionShiftError.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DilutedSpinGlass.DepthAverage.average_add_eq line 12
2. def OAI.DilutedSpinGlass.ReducedTopology.projectionShiftError line 29
3. lemma OAI.DilutedSpinGlass.ReducedTopology.projectionShiftError_nonneg line 37
4. lemma OAI.DilutedSpinGlass.ReducedTopology.projectionShiftError_sq line 43
5. theorem OAI.DilutedSpinGlass.ReducedTopology.averaged_projectionShiftError_sq_le line 56

   Source documentation

   Literal normalized regular-assignment estimate (projection-shift-error). Constants depend ONLY on the reduced child topologies, not on kernels, spatial dimension, depth count, target histories, or extension choices.

   theorem averaged_projectionShiftError_sq_le (a : α) (C : ι → ReducedTopology)
       (e : (j : ι) → (C j).Vertex → {j : α // j≠a}) (he : ∀ j, Function.Injective (e j))
       (η : ℝ) (hlarge : 1<η*(L:ℝ)) (D : (α → Fin L) → Prop)
       (hD : ∀ Q, D Q → ∀ j, Admissible (C j) (fun v => (Q (e j v)).val) ((Q a).val+1) L ∧
         DepthAverage.Regular η (fun v => Q (e j v)))
       (T : KernelTower Ω L) (f : FinitePath Ω L → Fin N → ℝ) (hf : ∀ x i, |f x i|≤1) :
       DepthAverage.average D (fun Q => (projectionShiftError a C e T f Q)^2) ≤
         8*((Fintype.card ι:ℝ)*∑ j, (Fintype.card (C j).Vertex:ℝ)*
           (∑ v : (C j).Vertex, (vertexArity (C j) v:ℝ)^2)+(Fintype.card ι:ℝ)^2)/(L:ℝ) := by
   …

   Mentions: OAI.DilutedSpinGlass.ReducedTopology, OAI.DilutedSpinGlass.ReducedTopology.Vertex, OAI.DilutedSpinGlass.ReducedTopology.Admissible, OAI.DilutedSpinGlass.DepthAverage.Regular, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.DepthAverage.average, OAI.DilutedSpinGlass.ReducedTopology.projectionShiftError, OAI.DilutedSpinGlass.ReducedTopology.vertexArity

6. theorem OAI.DilutedSpinGlass.ReducedTopology.target_contraction_shift_le line 92

   Source documentation

   Every actual target history has contraction error at most this SAME h_N. No regularity or independence assumption on its union with the old tree.

   theorem target_contraction_shift_le (a : α) (C : ι → ReducedTopology)
       (e : (j : ι) → (C j).Vertex → {j : α // j≠a})
       (T : KernelTower Ω L) (f : FinitePath Ω L → Fin N → ℝ) (hf : ∀ x i, |f x i|≤1)
       (Q : α → Fin L) (Target : PrescribedTree L) (u v : Target.Leaf) :
       PrescribedTree.targetContractionChangeSq Target T u v
         (conditionalScheduledProduct L 0 ((Q a).val+1) C (fun j v => (Q (e j v)).val+1) T f)
         (conditionalScheduledProduct L 0 (Q a).val C (fun j v => (Q (e j v)).val) T f) ≤
           (projectionShiftError a C e T f Q)^2 := by
   …

   Mentions: OAI.DilutedSpinGlass.ReducedTopology, OAI.DilutedSpinGlass.ReducedTopology.Vertex, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.targetContractionChangeSq, OAI.DilutedSpinGlass.ReducedTopology.conditionalScheduledProduct, OAI.DilutedSpinGlass.ReducedTopology.projectionShiftError

7. theorem OAI.DilutedSpinGlass.ReducedTopology.matrixProjectionError_shift_le line 108

   Source documentation

   The universal shift error is valid in the literal matrix projection error, before taking signed histories or any physical-root expectation.

   theorem matrixProjectionError_shift_le {I : Type} [Fintype I] [DecidableEq I]
       (a : α) (C : ι → ReducedTopology)
       (e : (j : ι) → (C j).Vertex → {j : α // j≠a})
       (T : KernelTower Ω L) (f : FinitePath Ω L → Fin N → ℝ) (hf : ∀ x i, |f x i|≤1)
       (Q : α → Fin L) (Target : PrescribedTree L) (q : I → Target.Leaf) (u v : I)
       (A : (I → FinitePath Ω L) → ℝ) :
       PrescribedTree.matrixProjectionError Target q T u v A
         (conditionalScheduledProduct L 0 (Q a).val C (fun j w => (Q (e j w)).val) T f) ≤
       PrescribedTree.matrixProjectionError Target q T u v A
         (conditionalScheduledProduct L 0 ((Q a).val+1) C (fun j w => (Q (e j w)).val+1) T f)+
         projectionShiftError a C e T f Q := by
   …

   Mentions: OAI.DilutedSpinGlass.ReducedTopology, OAI.DilutedSpinGlass.ReducedTopology.Vertex, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.PrescribedTree.matrixProjectionError, OAI.DilutedSpinGlass.ReducedTopology.conditionalScheduledProduct, OAI.DilutedSpinGlass.ReducedTopology.projectionShiftError