OAI/Combinatorics/BinaryEdit/Distortion.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

Distortion of finite metric spaces under injective maps into real ℓ₁.

  1. def OAI.TreeEdit.BinaryLower.expansionRatios line 17

    Source documentation

    The two finite sets whose maxima define distortion.

    def expansionRatios (ρ : X → X → ℝ) (f : X → RealL1) : Set ℝ :=
…

    Mentions: OAI.TreeEdit.RealL1

  2. def OAI.TreeEdit.BinaryLower.contractionRatios line 20
  3. def OAI.TreeEdit.BinaryLower.embeddingDistortions line 23
  4. lemma OAI.TreeEdit.BinaryLower.expansionRatios_finite line 26
  5. lemma OAI.TreeEdit.BinaryLower.contractionRatios_finite line 32
  6. lemma OAI.TreeEdit.BinaryLower.expansionRatios_nonempty line 38
  7. lemma OAI.TreeEdit.BinaryLower.contractionRatios_nonempty line 43
  8. lemma OAI.TreeEdit.BinaryLower.expansion_nonneg line 48
  9. lemma OAI.TreeEdit.BinaryLower.contraction_nonneg line 55
  10. lemma OAI.TreeEdit.BinaryLower.distortion_nonneg line 62
  11. lemma OAI.TreeEdit.BinaryLower.exists_injective_L1 line 67

    Source documentation

    Every finite set admits an injection into the full sequence space.

    lemma exists_injective_L1 (X : Type*) [Finite X] :
    ∃ f : X → RealL1, Function.Injective f := by
…

    Mentions: OAI.TreeEdit.RealL1

  12. lemma OAI.TreeEdit.BinaryLower.embeddingDistortions_nonempty line 80
  13. lemma OAI.TreeEdit.BinaryLower.embeddingDistortions_bddBelow line 85
  14. lemma OAI.TreeEdit.BinaryLower.c1_nonneg line 92
  15. lemma OAI.TreeEdit.BinaryLower.c1_le_distortion line 98
  16. lemma OAI.TreeEdit.BinaryLower.le_c1 line 103
  17. lemma OAI.TreeEdit.BinaryLower.expansionRatios_comp_subset line 110
  18. lemma OAI.TreeEdit.BinaryLower.contractionRatios_comp_subset line 117
  19. lemma OAI.TreeEdit.BinaryLower.distortion_comp_le line 125

    Source documentation

    Restriction to an isometric subspace cannot increase distortion.

    lemma distortion_comp_le [Finite X] [Nontrivial X] [Finite Y] [Nontrivial Y]
    (ρ : X → X → ℝ) (σ : Y → Y → ℝ) (hσ : ∀ x y, 0 ≤ σ x y)
    (g : X → Y) (hg : Function.Injective g)
    (hiso : ∀ x y, σ (g x) (g y) = ρ x y) (f : Y → RealL1) :
    distortion ρ (f ∘ g) ≤ distortion σ f := by
…

    Mentions: OAI.TreeEdit.RealL1

  20. lemma OAI.TreeEdit.BinaryLower.c1_mono_isometry line 144

    Source documentation

    The optimal ℓ₁ distortion is monotone under injective isometries.

    lemma c1_mono_isometry [Finite X] [Nontrivial X] [Finite Y] [Nontrivial Y]
    (ρ : X → X → ℝ) (σ : Y → Y → ℝ) (hσ : ∀ x y, 0 ≤ σ x y)
    (g : X → Y) (hg : Function.Injective g)
    (hiso : ∀ x y, σ (g x) (g y) = ρ x y) :
    c1 X ρ ≤ c1 Y σ := by
…
  21. lemma OAI.TreeEdit.BinaryLower.c1_eq_of_equiv line 155
  22. lemma OAI.TreeEdit.BinaryLower.c1_le_of_bounds line 169

    Source documentation

    A noncontracting embedding with expansion at most D gives the usual upper bound on optimal distortion. No existence theorem is assumed here.

    lemma c1_le_of_bounds [Finite X] [Nontrivial X]
    (ρ : X → X → ℝ) (hρ : ∀ x y, 0 ≤ ρ x y)
    (hpos : ∀ x y, x ≠ y → 0 < ρ x y)
    (f : X → RealL1) (D : ℝ) (hD : 0 ≤ D)
    (hlower : ∀ x y, ρ x y ≤ ‖f x - f y‖)
    (hupper : ∀ x y, ‖f x - f y‖ ≤ D * ρ x y) :
    c1 X ρ ≤ D := by
…

    Mentions: OAI.TreeEdit.RealL1

  23. lemma OAI.TreeEdit.BinaryLower.distortion_comp_le_bilip line 199

    Source documentation

    Comparing two metrics through a scaled bi-Lipschitz injection costs only its ratio of expansion to contraction in the distortion product.

    lemma distortion_comp_le_bilip [Finite X] [Nontrivial X] [Finite Y] [Nontrivial Y]
    (ρ : X → X → ℝ) (σ : Y → Y → ℝ)
    (hρ : ∀ x y, 0 ≤ ρ x y) (hσ : ∀ x y, 0 ≤ σ x y)
    (hpos : ∀ x y, x ≠ y → 0 < ρ x y)
    (g : X → Y) (hg : Function.Injective g)
    (a b : ℝ) (ha : 0 < a) (hb : 0 ≤ b)
    (hlower : ∀ x y, a * ρ x y ≤ σ (g x) (g y))
    (hupper : ∀ x y, σ (g x) (g y) ≤ b * ρ x y) (f : Y → RealL1) :
    distortion ρ (f ∘ g) ≤ (b / a) * distortion σ f := by
…

    Mentions: OAI.TreeEdit.RealL1

  24. lemma OAI.TreeEdit.BinaryLower.c1_le_bilip_mul line 255

    Source documentation

    Optimal distortion transfer through any scaled bi-Lipschitz injection. In particular, a=P/804 and b=P give constant distortion loss.

    lemma c1_le_bilip_mul [Finite X] [Nontrivial X] [Finite Y] [Nontrivial Y]
    (ρ : X → X → ℝ) (σ : Y → Y → ℝ)
    (hρ : ∀ x y, 0 ≤ ρ x y) (hσ : ∀ x y, 0 ≤ σ x y)
    (hpos : ∀ x y, x ≠ y → 0 < ρ x y)
    (g : X → Y) (hg : Function.Injective g)
    (a b : ℝ) (ha : 0 < a) (hb : 0 < b)
    (hlower : ∀ x y, a * ρ x y ≤ σ (g x) (g y))
    (hupper : ∀ x y, σ (g x) (g y) ≤ b * ρ x y) :
    c1 X ρ ≤ (b / a) * c1 Y σ := by
…
  25. lemma OAI.TreeEdit.BinaryLower.exists_normalized_embedding line 278

    Source documentation

    Rescaling by the maximal contraction ratio makes an injective embedding noncontracting without changing the distortion bound.

    lemma exists_normalized_embedding [Finite X] [Nontrivial X]
    (ρ : X → X → ℝ) (hρ : ∀ x y, 0 ≤ ρ x y)
    (hdiag : ∀ x, ρ x x = 0) (hpos : ∀ x y, x ≠ y → 0 < ρ x y)
    (f : X → RealL1) (hf : Function.Injective f) :
    ∃ g : X → RealL1, Function.Injective g ∧
      ∀ x y, ρ x y ≤ ‖g x - g y‖ ∧ ‖g x - g y‖ ≤ distortion ρ f * ρ x y := by
…

    Mentions: OAI.TreeEdit.RealL1

  26. lemma OAI.TreeEdit.BinaryLower.le_c1_of_normalized line 319

    Source documentation

    An obstruction proved for all normalized embeddings gives a lower bound on the infimum defining c1. This is the passage used by the two tree routes.

    lemma le_c1_of_normalized [Finite X] [Nontrivial X]
    (ρ : X → X → ℝ) (hρ : ∀ x y, 0 ≤ ρ x y)
    (hdiag : ∀ x, ρ x x = 0) (hpos : ∀ x y, x ≠ y → 0 < ρ x y)
    (D : ℝ)
    (hobstruction : ∀ (g : X → RealL1) (A : ℝ),
      (∀ x y, ρ x y ≤ ‖g x - g y‖ ∧ ‖g x - g y‖ ≤ A * ρ x y) → D ≤ A) :
    D ≤ c1 X ρ := by
…

    Mentions: OAI.TreeEdit.RealL1

  27. lemma OAI.TreeEdit.BinaryLower.exists_nonexpanding_embedding line 333

    Source documentation

    The dual normalization used verbatim by the finite-tree obstruction: the image distance lies between ρ / distortion and ρ.

    lemma exists_nonexpanding_embedding [Finite X] [Nontrivial X]
    (ρ : X → X → ℝ) (hρ : ∀ x y, 0 ≤ ρ x y)
    (hdiag : ∀ x, ρ x x = 0) (hpos : ∀ x y, x ≠ y → 0 < ρ x y)
    (f : X → RealL1) (hf : Function.Injective f) :
    0 < distortion ρ f ∧ ∃ g : X → RealL1, Function.Injective g ∧
      ∀ x y, ρ x y / distortion ρ f ≤ ‖g x - g y‖ ∧ ‖g x - g y‖ ≤ ρ x y := by
…

    Mentions: OAI.TreeEdit.RealL1

  28. lemma OAI.TreeEdit.BinaryLower.le_c1_of_nonexpanding line 365