OAI/Analysis/TreePotential/SegmentEndpoints.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BoundedTreePotentials.Segments.norm_weighted_signed_sum line 16
2. lemma OAI.BoundedTreePotentials.Segments.mixture_replacement_error line 25
3. lemma OAI.BoundedTreePotentials.Segments.unsigned_energy_bound_on line 48
4. lemma OAI.BoundedTreePotentials.Segments.mixture_replacement_norm line 61
5. lemma OAI.BoundedTreePotentials.Segments.finite_mixture_tail_scalar line 86
6. theorem OAI.BoundedTreePotentials.Segments.finite_mixture_tail line 103

   Source documentation

   The finite-state endpoint argument: replacement, actual exit cancellation, unsigned mass, and both approximation errors appear explicitly.

   theorem finite_mixture_tail [Nonempty I]
       {E : Finset Node} (hE : Initial (E : Set Node)) (x y : DualCore)
       (hx : completedHead unitTests E x=x) (g : unitTests)
       (hsupp : ∀ v ∉ E, g.val v=0) (hgn : completedTestFunctional unitTests g x=‖x‖)
       (A : I → Atom) (p σ : I → ℝ) (hp : ∀ i, 0 ≤ p i) (hp1 : ∑ i, p i=1)
       (hσ : ∀ i, |σ i| ≤ 1) {e : ℝ} (he : 0 ≤ e)
       (hmean : ‖(∑ i, p i • (A i).inCore)-x‖ ≤ e)
       (hsigned : ‖(∑ i, (p i*σ i) • (A i).inCore)-y‖ ≤ e) :
       ‖completedTail unitTests E y‖ ≤
         2*e+(Real.sqrt 2+Real.sqrt 6)*Real.sqrt (1-‖x‖+e) := by
   …

   Mentions: OAI.BoundedTreePotentials.Segments.Node, OAI.BoundedTreePotentials.Segments.Initial, OAI.BoundedTreePotentials.Segments.DualCore, OAI.BoundedTreePotentials.completedHead, OAI.BoundedTreePotentials.Segments.unitTests, OAI.BoundedTreePotentials.completedTestFunctional, OAI.BoundedTreePotentials.Segments.Atom, OAI.BoundedTreePotentials.completedTail

7. lemma OAI.BoundedTreePotentials.Segments.exists_atom_distribution line 171
8. lemma OAI.BoundedTreePotentials.Segments.endpoint_atom_distribution line 192

   Source documentation

   Both endpoint distributions are combined without requiring a common finite index set, or assuming an attained atomic decomposition.

   lemma endpoint_atom_distribution (x y : DualCore) (hp : ‖x+y‖ ≤ 1) (hm : ‖x-y‖ ≤ 1)
       {e : ℝ} (he : 0 < e) :
       ∃ (I : Type) (_ : Fintype I) (_ : Nonempty I) (p σ : I → ℝ) (A : I → Atom),
         (∀ i, 0 ≤ p i) ∧ (∑ i, p i)=1 ∧ (∀ i, |σ i| ≤ 1) ∧
         ‖(∑ i, p i • (A i).inCore)-x‖ ≤ e ∧
         ‖(∑ i, (p i*σ i) • (A i).inCore)-y‖ ≤ e := by
   …

   Mentions: OAI.BoundedTreePotentials.Segments.DualCore, OAI.BoundedTreePotentials.Segments.Atom

9. theorem OAI.BoundedTreePotentials.Segments.incomparable_tail_core line 245

   Source documentation

   The incomparable tail bound on the polar completion, without finite-support assumptions. Its full-dual formulation follows from the core/full-dual identification.

   theorem incomparable_tail_core {E : Finset Node} (hE : Initial (E : Set Node))
       (x y : DualCore) (hx : completedHead unitTests E x=x)
       (hp : ‖x+y‖ ≤ 1) (hm : ‖x-y‖ ≤ 1) :
       ‖completedTail unitTests E y‖ ≤ (Real.sqrt 2+Real.sqrt 6)*Real.sqrt (1-‖x‖) := by
   …

   Mentions: OAI.BoundedTreePotentials.Segments.Node, OAI.BoundedTreePotentials.Segments.Initial, OAI.BoundedTreePotentials.Segments.DualCore, OAI.BoundedTreePotentials.completedHead, OAI.BoundedTreePotentials.Segments.unitTests, OAI.BoundedTreePotentials.completedTail