OAI/Analysis/DiamondDistortion/PathBounds.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DiamondDistortion.Midpoint.tail_packing line 18

   Source documentation

   Packing with one finite-rank head and a common tail bound; no head norm estimate and no attained infinite minimum is used.

   lemma tail_packing (P : X →L[ℝ] X) [FiniteDimensional ℝ (LinearMap.range P.toLinearMap)]
       (z : ℕ → X) {R ε T : ℝ} (hz : ∀ i,‖z i‖ ≤ R)
       (hs : ∀ i j,i ≠ j → ε ≤ ‖z i-z j‖) (ht : ∀ i,‖z i-P (z i)‖ ≤ T) :
       ε/2 ≤ T := by
   …

2. def OAI.DiamondDistortion.PathApplications.RelativeInput line 50

   Source documentation

   Threshold-removal uses a single head for all deviations at this radius.

   def RelativeInput (A : Heads ι X) : Prop :=
   …

3. def OAI.DiamondDistortion.PathApplications.relativeDelta line 55
4. lemma OAI.DiamondDistortion.PathApplications.relative_parameters line 57
5. lemma OAI.DiamondDistortion.PathApplications.relative_lens_impossible line 71
6. lemma OAI.DiamondDistortion.PathApplications.relative_actual_child line 87

   Source documentation

   An actual original child exceeds the relative factor, rather than merely a quotient representative or a supremum satisfying a non-strict bound.

   lemma relative_actual_child (A : Heads ι X) (hinput : RelativeInput A)
       {D : ℝ} (hD : 1 ≤ D) {x : X} (z : ℕ → X) (hx : 1 ≤ ‖x‖) (hxD : ‖x‖ ≤ D)
       (hs : ∀ i j,i ≠ j → 2 ≤ ‖z i-z j‖) :
       ∃ i,(1+relativeDelta D)*‖x‖ < max ‖x+z i‖ ‖x-z i‖ := by
   …

   Mentions: OAI.DiamondDistortion.PathApplications.RelativeInput, OAI.DiamondDistortion.PathApplications.relativeDelta

7. theorem OAI.DiamondDistortion.PathApplications.relative_cost line 95
8. lemma OAI.DiamondDistortion.Midpoint.bounded_scalar_subsequence line 126
9. lemma OAI.DiamondDistortion.Midpoint.bounded_weak_pair line 142
10. def OAI.DiamondDistortion.PathApplications.WeakInput line 158
11. lemma OAI.DiamondDistortion.PathApplications.weak_lens line 163
12. theorem OAI.DiamondDistortion.PathApplications.weak_linear line 190