ParameterImage.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Lower distortion bounds on the finite image of a parameter space.

def OAI.TreeEdit.BinaryLower.ParameterImage.image line 14
Source documentation
The actual finite image of a finite parameter space.
```
def image (G : A → X) : Finset X := by
…
```
lemma OAI.TreeEdit.BinaryLower.ParameterImage.mem_image line 18
def OAI.TreeEdit.BinaryLower.ParameterImage.toImage line 23
Source documentation
The canonical map onto the finite image, allowing state-to-word collisions.
```
def toImage (G : A → X) (a : A) : {x : X // x ∈ image G} :=
…
```
Mentions: OAI.TreeEdit.BinaryLower.ParameterImage.image
lemma OAI.TreeEdit.BinaryLower.ParameterImage.image_card_two line 26

theorem OAI.TreeEdit.BinaryLower.ParameterImage.image_lower_of_nonexpanding_obstruction line 36

Source documentation

An obstruction for every normalized map on parameter states gives the claimed distortion lower bound on the finite image, even when G is not injective. All metric hypotheses are the ordinary ones needed to normalize.

theorem image_lower_of_nonexpanding_obstruction
    (G : A → X) (hG : ∃ a b, G a ≠ G b)
    (ρ : X → X → ℝ) (hρ : ∀ x y, 0 ≤ ρ x y)
    (hdiag : ∀ x, ρ x x = 0) (hpos : ∀ x y, x ≠ y → 0 < ρ x y)
    (D : ℝ)
    (hobstruction : ∀ (F : A → RealL1) (C : ℝ), 0 < C →
      (∀ a b, ρ (G a) (G b) / C ≤ ‖F a - F b‖ ∧
        ‖F a - F b‖ ≤ ρ (G a) (G b)) → D ≤ C) :
    2 ≤ (image G).card ∧
      D ≤ c1 {x : X // x ∈ image G} (fun x y => ρ x.val y.val) := by
…

Mentions: OAI.TreeEdit.RealL1, OAI.TreeEdit.BinaryLower.ParameterImage.image

theorem OAI.TreeEdit.BinaryLower.ParameterImage.exists_word_image_lower line 60

Source documentation

The finite-image obstruction for ordinary edit distance on fixed-length words.

theorem exists_word_image_lower {Γ : Type*} {n : ℕ}
    (G : A → Word Γ n)
    (hsep : ∃ a b, 0 < ed (G a).val (G b).val)
    (D : ℝ)
    (hobstruction : ∀ (F : A → RealL1) (C : ℝ), 0 < C →
      (∀ a b, (ed (G a).val (G b).val : ℝ) / C ≤ ‖F a - F b‖ ∧
        ‖F a - F b‖ ≤ (ed (G a).val (G b).val : ℝ)) → D ≤ C) :
    ∃ W : Finset (Word Γ n),
      (∀ w, w ∈ W ↔ ∃ a, G a = w) ∧ 2 ≤ W.card ∧
      D ≤ c1 {w : Word Γ n // w ∈ W}
        (fun x y => (ed x.val.val y.val.val : ℝ)) := by
…

Mentions: OAI.TreeEdit.Word, OAI.TreeEdit.ed, OAI.TreeEdit.RealL1

theorem OAI.TreeEdit.BinaryLower.ParameterImage.exists_binary_image_lower line 86

Source documentation

The binary image has exactly the binarySetDistortion of the binary word metric.

theorem exists_binary_image_lower {n : ℕ}
    (G : A → Word Bool n)
    (hsep : ∃ a b, 0 < ed (G a).val (G b).val)
    (D : ℝ)
    (hobstruction : ∀ (F : A → RealL1) (C : ℝ), 0 < C →
      (∀ a b, (ed (G a).val (G b).val : ℝ) / C ≤ ‖F a - F b‖ ∧
        ‖F a - F b‖ ≤ (ed (G a).val (G b).val : ℝ)) → D ≤ C) :
    ∃ W : Finset (Word Bool n),
      (∀ w, w ∈ W ↔ ∃ a, G a = w) ∧ 2 ≤ W.card ∧ D ≤ binarySetDistortion W := by
…

Mentions: OAI.TreeEdit.Word, OAI.TreeEdit.ed, OAI.TreeEdit.RealL1

theorem OAI.TreeEdit.BinaryLower.ParameterImage.exists_word_image_lower_of_root_bound line 100

Source documentation

Final finite-tree passage: the distinguished root displacement is far in every state, but every nonexpanding ℓ₁ map has a small average root displacement. The resulting lower bound concerns the actual word image.

theorem exists_word_image_lower_of_root_bound {Γ : Type*} {n : ℕ}
    [AddCommGroup A] (G : A → Word Γ n) (z : A)
    (lower upper : ℝ) (hlower : 0 < lower) (hupper : 0 < upper)
    (hsep : ∀ x, lower ≤ (ed (G x).val (G (x + z)).val : ℝ))
    (hroot : ∀ F : A → RealL1,
      (∀ x y, ‖F x - F y‖ ≤ (ed (G x).val (G y).val : ℝ)) →
      (∑ x : A, ‖F (x + z) - F x‖) / Fintype.card A ≤ upper) :
    ∃ W : Finset (Word Γ n),
      (∀ w, w ∈ W ↔ ∃ a, G a = w) ∧ 2 ≤ W.card ∧
      lower / upper ≤ c1 {w : Word Γ n // w ∈ W}
        (fun x y => (ed x.val.val y.val.val : ℝ)) := by
…

Mentions: OAI.TreeEdit.Word, OAI.TreeEdit.ed, OAI.TreeEdit.RealL1