Backward.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.DiamondDistortion.Midpoint.lens_shrink line 18

Source documentation

Symmetry and convexity along a ray, proved by the explicit two-endpoint convex combinations.

lemma lens_shrink {a R : ℝ} (ha : 0 ≤ a) (ha1 : a ≤ 1) (u v : X)
    (hp : ‖u+v‖ ≤ R) (hm : ‖u-v‖ ≤ R) :
    max ‖u+a • v‖ ‖u-a • v‖ ≤ R := by
…

def OAI.DiamondDistortion.Midpoint.LocalQuotientGain line 41
Source documentation
The unit-sphere finite-codimensional version of the local midpoint input.
```
def LocalQuotientGain (X : Type*) [NormedAddCommGroup X] [NormedSpace ℝ X]
    (t g : ℝ) : Prop :=
…
```
lemma OAI.DiamondDistortion.Midpoint.LocalQuotientGain.large_step line 47
def OAI.DiamondDistortion.Midpoint.Cof line 65
Source documentation
Closed finite-codimensional subspaces, with the two conditions separately retained, not replaced by a coordinate-null convention.
```
def Cof (X : Type*) [NormedAddCommGroup X] [NormedSpace ℝ X] :=
…
```
def OAI.DiamondDistortion.Midpoint.maximumModulus line 68
def OAI.DiamondDistortion.Midpoint.AMUC line 73
lemma OAI.DiamondDistortion.Midpoint.positive_modulus_gain line 76
theorem OAI.DiamondDistortion.Diamond.amuc_obstruction line 111
Source documentation
AMUC forbids a single distortion bound for the normalized countably branching diamonds. Finite dimensional spaces are automatically covered as well.
```
theorem amuc_obstruction (hX : Midpoint.AMUC X) : ¬ UniformEmbeddings X := by
…
```
Mentions: OAI.DiamondDistortion.Midpoint.AMUC, OAI.DiamondDistortion.Diamond.UniformEmbeddings
lemma OAI.DiamondDistortion.Diamond.equivalent_distortion line 132
Source documentation
Transport of distortion under exact two-sided norm equivalence. The linear equivalence is simply the identification of the original space with its equivalent-norm copy; there is no change of graph or choice of scales.
```
lemma equivalent_distortion (e : X ≃ₗ[ℝ] Y) {a b : ℝ} (ha : 0 < a) (hb : 0 < b)
    (he : ∀ x : X,a*‖x‖ ≤ ‖e x‖ ∧ ‖e x‖ ≤ b*‖x‖)
    {k : ℕ} (f : Vertex k → X) {D s : ℝ} (hf : HasDistortion k f D s) :
    HasDistortion k (fun v => e (f v)) ((b/a)*D) (a*s) := by
…
```
Mentions: OAI.DiamondDistortion.Diamond.Vertex, OAI.DiamondDistortion.Diamond.HasDistortion
theorem OAI.DiamondDistortion.Diamond.equivalent_amuc line 156