EncodedImage.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Distortion transport through finite images of fixed-width codes.

def OAI.TreeEdit.BinaryLower.encodedWord line 15
Source documentation
The concatenation extension, viewed in its exact-length target type.
```
def encodedWord {α : Type u} {M P : ℕ} (c : α → Word Bool P)
    (x : Word α M) : Word Bool (M * P) :=
…
```
Mentions: OAI.TreeEdit.Word
def OAI.TreeEdit.BinaryLower.encodedSet line 20
Source documentation
The actual finite image, rather than an abstract copy of the source set.
```
def encodedSet {α : Type u} {M P : ℕ} (c : α → Word Bool P)
    (W : Finset (Word α M)) : Finset (Word Bool (M * P)) :=
…
```
Mentions: OAI.TreeEdit.Word
lemma OAI.TreeEdit.BinaryLower.encodedWord_injective_of_lower line 24
lemma OAI.TreeEdit.BinaryLower.encodedSet_card line 39
def OAI.TreeEdit.BinaryLower.encodedMember line 49
Source documentation
The map from source membership witnesses into membership witnesses of the encoded finite set, with no choice of an inverse.
```
def encodedMember {α : Type u} {M P : ℕ} (c : α → Word Bool P)
    (W : Finset (Word α M)) : {x : Word α M // x ∈ W} →
      {y : Word Bool (M * P) // y ∈ encodedSet c W} :=
…
```
Mentions: OAI.TreeEdit.Word, OAI.TreeEdit.BinaryLower.encodedSet
lemma OAI.TreeEdit.BinaryLower.encodedMember_injective line 54

lemma OAI.TreeEdit.BinaryLower.c1_le_encodedSet_mul line 66

Source documentation

Distortion transport for the concrete finite image of a bi-Lipschitz code.

lemma c1_le_encodedSet_mul {α : Type u} {M P : ℕ}
    (c : α → Word Bool P) (W : Finset (Word α M)) (hW : 2 ≤ W.card)
    {a b : ℝ} (ha : 0 < a) (hb : 0 < b)
    (hlower : ∀ x y : Word α M,
      a * (ed x.val y.val : ℝ) ≤
        (ed (encode c x.val) (encode c y.val) : ℝ))
    (hupper : ∀ x y : Word α M,
      (ed (encode c x.val) (encode c y.val) : ℝ) ≤
        b * (ed x.val y.val : ℝ)) :
    c1 {x : Word α M // x ∈ W}
      (fun x y => (ed x.val.val y.val.val : ℝ)) ≤
        (b / a) * binarySetDistortion (encodedSet c W) := by
…

Mentions: OAI.TreeEdit.Word, OAI.TreeEdit.ed, OAI.TreeEdit.encode, OAI.TreeEdit.BinaryLower.encodedSet

lemma OAI.TreeEdit.BinaryLower.c1_le_804_encodedSet line 102

Source documentation

The scale cancels: lower factor P/804 and upper factor P lose only 804.

lemma c1_le_804_encodedSet {α : Type u} {M P : ℕ}
    (c : α → Word Bool P) (hP : 0 < P)
    (W : Finset (Word α M)) (hW : 2 ≤ W.card)
    (hlower : ∀ x y : Word α M,
      ((P : ℝ) / 804) * (ed x.val y.val : ℝ) ≤
        (ed (encode c x.val) (encode c y.val) : ℝ)) :
    c1 {x : Word α M // x ∈ W}
      (fun x y => (ed x.val.val y.val.val : ℝ)) ≤
        804 * binarySetDistortion (encodedSet c W) := by
…

Mentions: OAI.TreeEdit.Word, OAI.TreeEdit.ed, OAI.TreeEdit.encode, OAI.TreeEdit.BinaryLower.encodedSet

theorem OAI.TreeEdit.BinaryLower.exists_binary_image_of_code line 119

Source documentation

Existential form used by the finite-tree binary-family construction.

theorem exists_binary_image_of_code {α : Type u} {M P : ℕ}
    (c : α → Word Bool P) (hP : 0 < P)
    (W : Finset (Word α M)) (hW : 2 ≤ W.card)
    (hlower : ∀ x y : Word α M,
      ((P : ℝ) / 804) * (ed x.val y.val : ℝ) ≤
        (ed (encode c x.val) (encode c y.val) : ℝ)) :
    ∃ V : Finset (Word Bool (M * P)), 2 ≤ V.card ∧
      c1 {x : Word α M // x ∈ W}
        (fun x y => (ed x.val.val y.val.val : ℝ)) / 804 ≤
          binarySetDistortion V := by
…

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