OAI/Analysis/DiamondDistortion/AMUC.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DiamondDistortion.Diamond.old_upper line 16
2. def OAI.DiamondDistortion.Diamond.FixedBoundGain line 22
3. lemma OAI.DiamondDistortion.Diamond.actual_additive_growth line 27
4. theorem OAI.DiamondDistortion.Diamond.fixed_bound line 64
5. lemma OAI.DiamondDistortion.Diamond.fixed_bound_of_quadratic line 78

   Source documentation

   The unconditional segment lens supplies the fixed-distortion bounded-family input as well, with a concrete positive choice of c_D.

   lemma fixed_bound_of_quadratic {X : Type*} [NormedAddCommGroup X] [NormedSpace ℝ X] (hX : QuadraticLens X) {D : ℝ} (hD : 1 ≤ D) :
       FixedBoundGain X D (1/(64*D)) := by
   …

   Mentions: OAI.DiamondDistortion.Diamond.QuadraticLens, OAI.DiamondDistortion.Diamond.FixedBoundGain

6. def OAI.DiamondDistortion.Diamond.UniformEmbeddings line 98

   Source documentation

   Uniform distortion means one finite constant, with a separate map and a separate positive scale for each depth.

   def UniformEmbeddings (X : Type*) [NormedAddCommGroup X] : Prop :=
   …

7. theorem OAI.DiamondDistortion.atomic_distortion line 103
8. theorem OAI.DiamondDistortion.direct_atomic_obstruction line 109
9. theorem OAI.DiamondDistortion.infinite_obstruction line 116