FiniteWordL1Mean.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The actual finite word's averaged ℓ₁ displacement

This specializes the proved finite-group Fourier obstruction to the concrete cyclic parameter space and recursive word evaluator. The only metric input is that the chosen map into actual ℓ₁ does not expand ordinary edit distance.

theorem OAI.TreeEdit.BinaryLower.FiniteTree.finiteWord_leaf_l1_cost line 24

Source documentation

The leaf cyclic tests have the required pointwise cost for every map which is nonexpanding on pairs of actual finite words.

theorem finiteWord_leaf_l1_cost {m k : ℕ}
    (p : Fin k → Fin m → ℕ) (i₀ : Fin m) (T : ℕ)
    (F : State (wordPeriods p) → RealL1)
    (hF : ∀ x y, ‖F x - F y‖ ≤
      (ed (finiteWord p i₀ T k [] x) (finiteWord p i₀ T k [] y) : ℝ))
    (a : Fin k → Fin m) [NeZero (FiniteVectors.leafPeriod p a)]
    (z : ZMod (FiniteVectors.leafPeriod p a)) (x : State (wordPeriods p)) :
    ‖F (x + wordLeafCoordinate p a z) - F x‖ ≤
      ((m * T : ℕ) : ℝ) ^ k / (m : ℝ) ^ k := by
…

Mentions: OAI.TreeEdit.BinaryLower.FiniteTree.State, OAI.TreeEdit.BinaryLower.FiniteTree.wordPeriods, OAI.TreeEdit.RealL1, OAI.TreeEdit.ed, OAI.TreeEdit.BinaryLower.FiniteTree.finiteWord, OAI.TreeEdit.BinaryLower.FiniteVectors.leafPeriod, OAI.TreeEdit.BinaryLower.FiniteTree.wordLeafCoordinate

theorem OAI.TreeEdit.BinaryLower.FiniteTree.finiteWord_root_mean_bound line 41

Source documentation

The actual finite word satisfies the full Fourier root estimate. All leaf costs and sparse-node tests are proved from its concrete construction.

theorem finiteWord_root_mean_bound {m k : ℕ}
    (p : Fin k → Fin m → ℕ) (i₀ : Fin m) (hk : 1 ≤ k)
    (hppos : ∀ q i, 0 < p q i) (hp : ∀ q i, p q i ≤ k ^ 5)
    (T : ℕ) (hT : 0 < T) (hJT : 4 * k ^ (10 * k) ≤ T)
    [Fintype (State (wordPeriods p))]
    (F : State (wordPeriods p) → RealL1)
    (hF : ∀ x y, ‖F x - F y‖ ≤
      (ed (finiteWord p i₀ T k [] x) (finiteWord p i₀ T k [] y) : ℝ)) :
    (𝔼 x : State (wordPeriods p), ‖F (x + wordW p i₀ []) - F x‖) ≤
      4 * ((k : ℝ) * ((2 * ((4 * k ^ (10 * k) : ℕ) : ℝ) / T) *
        ((m * T : ℕ) : ℝ) ^ k) +
        ((m * T : ℕ) : ℝ) ^ k / (2 * (k : ℝ) ^ k)) := by
…

theorem OAI.TreeEdit.BinaryLower.FiniteTree.finiteWord_root_mean_bound34 line 90

Source documentation

The source parameter choice gives the explicit 34 M/k^k averaged root bound for every nonexpanding map of the actual constructed word image.

theorem finiteWord_root_mean_bound34 {m k : ℕ}
    (p : Fin k → Fin m → ℕ) (i₀ : Fin m) (hk : 2 ≤ k)
    (hppos : ∀ q i, 0 < p q i) (hp : ∀ q i, p q i ≤ k ^ 5)
    [Fintype (State (wordPeriods p))]
    (F : State (wordPeriods p) → RealL1)
    (hF : ∀ x y, ‖F x - F y‖ ≤
      (ed (finiteWord p i₀ (k ^ (20 * k)) k [] x)
        (finiteWord p i₀ (k ^ (20 * k)) k [] y) : ℝ)) :
    (𝔼 x : State (wordPeriods p), ‖F (x + wordW p i₀ []) - F x‖) ≤
      34 * ((m * k ^ (20 * k) : ℕ) : ℝ) ^ k / (k : ℝ) ^ k := by
…