FiniteL1Tree.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Actual ℓ₁ maps and the finite-tree obstruction

The finite-group displacement identity yields the finite-tree root estimate from geometric bounds on the concrete translations.

theorem OAI.TreeEdit.BinaryLower.FiniteActivity.finite_tree_l1_mean_bound line 23

Source documentation

Leaf periods, sparse-character detection and translation-cost bounds imply the root averaged-distance estimate for arbitrary maps into ℓ₁.

theorem finite_tree_l1_mean_bound {A σ : Type*}
    [AddCommGroup A] [Fintype A] [Fintype σ] [Nonempty σ]
    (m b h : ℕ) (hm : m ≠ 0) (hb : 0 < b)
    (w : List (Fin m) → A)
    (Q : (Fin h → Fin m) → ℕ) [∀ f, NeZero (Q f)]
    (φ : ∀ f, ZMod (Q f) →+ A)
    (hgen : ∀ f : Fin h → Fin m, w (List.ofFn f) = φ f 1)
    (F : A → RealL1)
    (shift : InternalNode (Fin m) h → σ → A) (M C : ℝ)
    (hleaf : ∀ f (z : ZMod (Q f)) x,
      ‖F (x + φ f z) - F x‖ ≤ M / (m : ℝ) ^ h)
    (hdetect : ∀ v χ, characterSparse w b v χ →
…

Mentions: OAI.TreeEdit.RealL1, OAI.TreeEdit.BinaryLower.FiniteActivity.InternalNode, OAI.TreeEdit.BinaryLower.FiniteActivity.characterSparse

theorem OAI.TreeEdit.BinaryLower.FiniteActivity.source_mean_bound34 line 54

Source documentation

Parameter normalization gives the root estimate with the absolute constant 34.

theorem source_mean_bound34 {A : Type*} [AddCommGroup A] [Fintype A]
    (F : A → RealL1) (root : A) {k : ℕ} {M : ℝ}
    (hk : 1 ≤ k) (hM : 0 ≤ M)
    (hroot : (𝔼 x : A, ‖F (x + root) - F x‖) ≤
      4 * ((k : ℝ) * ((2 * (4 * (k : ℝ) ^ (10 * k)) /
        (k : ℝ) ^ (20 * k)) * M) + M / (2 * (k : ℝ) ^ k))) :
    (𝔼 x : A, ‖F (x + root) - F x‖) ≤ 34 * M / (k : ℝ) ^ k := by
…

Mentions: OAI.TreeEdit.RealL1