OAI/Analysis/DiamondDistortion/Stretch.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DiamondDistortion.Diamond.norm_center_le line 16
2. lemma OAI.DiamondDistortion.Diamond.norm_deviation_le line 26
3. lemma OAI.DiamondDistortion.Diamond.slope_lower line 30
4. lemma OAI.DiamondDistortion.Diamond.slope_upper line 39
5. lemma OAI.DiamondDistortion.Diamond.old_lower line 48
6. lemma OAI.DiamondDistortion.Diamond.iterate_contraction line 56

   Source documentation

   Abstract multiplicative backward iteration, retaining every all-pairs lower bound and making no assertion of an attained stage supremum.

   lemma iterate_contraction {s D c : ℝ} (hc : 0 ≤ c) (hc1 : c ≤ 1)
       (hstep : ∀ (x : X) (z : ℕ → X) (R : ℝ),0 ≤ R → R ≤ D → s ≤ ‖x‖ →
         (∀ i,‖x+z i‖ ≤ R) → (∀ i,‖x-z i‖ ≤ R) →
         (∀ i j,i ≠ j → 2*s ≤ ‖z i-z j‖) → ‖x‖ ≤ c*R)
       (k : ℕ) (f : Vertex k → X) {L : ℝ} (hL : 0 ≤ L) (hLD : L ≤ D)
       (hl : ∀ u v,s*distance k u v ≤ ‖f u-f v‖)
       (hb : ∀ e,‖slope f e‖ ≤ L) : s ≤ c^k*L := by
   …

   Mentions: OAI.DiamondDistortion.Diamond.Vertex, OAI.DiamondDistortion.Diamond.distance, OAI.DiamondDistortion.Diamond.slope

7. lemma OAI.DiamondDistortion.Diamond.iterate_additive line 80

   Source documentation

   Abstract additive backward iteration. The existence of old edges ensures nonnegativity of each improved bound, including the last nonempty stage.

   lemma iterate_additive {s D δ : ℝ} (hδ : 0 ≤ δ)
       (hstep : ∀ (x : X) (z : ℕ → X) (R : ℝ),0 ≤ R → R ≤ D → s ≤ ‖x‖ →
         (∀ i,‖x+z i‖ ≤ R) → (∀ i,‖x-z i‖ ≤ R) →
         (∀ i j,i ≠ j → 2*s ≤ ‖z i-z j‖) → ‖x‖ ≤ R-δ)
       (k : ℕ) (f : Vertex k → X) {L : ℝ} (hL : 0 ≤ L) (hLD : L ≤ D)
       (hl : ∀ u v,s*distance k u v ≤ ‖f u-f v‖)
       (hb : ∀ e,‖slope f e‖ ≤ L) : s+(k:ℝ)*δ ≤ L := by
   …

   Mentions: OAI.DiamondDistortion.Diamond.Vertex, OAI.DiamondDistortion.Diamond.distance, OAI.DiamondDistortion.Diamond.slope

8. def OAI.DiamondDistortion.Diamond.SquareLens line 103
9. lemma OAI.DiamondDistortion.Diamond.squared_stretch_loss_general line 108
10. lemma OAI.DiamondDistortion.Diamond.squared_transfer line 139
11. lemma OAI.DiamondDistortion.Diamond.normalized_distortion line 152
12. lemma OAI.DiamondDistortion.Diamond.upper_one_normalization line 167
13. def OAI.DiamondDistortion.Diamond.RadialLens line 184
14. theorem OAI.DiamondDistortion.Diamond.radial_transfer line 189
15. def OAI.DiamondDistortion.Diamond.UnitLensBound line 218
16. theorem OAI.DiamondDistortion.Diamond.backward line 222