BoundedInverseCoding.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Continuous generator coding on a whole bounded logarithmic box

A continuous local inverse suffices: divide the logarithm by a fixed integer, use the local inverse, and repeat its word. This keeps the combinatorial pattern fixed and makes every amplitude continuous on the entire prescribed box. In particular, these selectors can be sampled independently of the starting sheet.

theorem OAI.PolycyclicRecognition.bounded_continuous_generator_coding line 25

Source documentation

Upgrade a continuous small-logarithm scheme to any fixed bounded box, without a measurable-selection theorem or a parameter-dependent word length.

theorem bounded_continuous_generator_coding
    (X : I → L) (Exp : L → G) (q : V →ₗ[ℝ] L)
    (hzero : Exp 0 = 1)
    (hadd : ∀ v (s t : ℝ), Exp ((s + t) • v) = Exp (s • v) * Exp (t • v))
    {ε : ℝ} {N : ℕ} {C : ℝ}
    {d : ℕ} (w : Fin d → List (I × ℝ)) (i : Fin d → I)
    (σ : V → Fin d → ℝ) (hσ : ContinuousOn σ (ball 0 ε))
    (hlocal : ∀ y ∈ ball (0 : V) ε,
      (generatorSchemeWord w i (σ y)).length ≤ N ∧
      (∀ z ∈ generatorSchemeWord w i (σ y), |z.2| ≤ C) ∧
      generatorGroupWord X Exp (generatorSchemeWord w i (σ y)) = Exp (q y))
    (R : ℝ) (hR : 0 ≤ R) (k : ℕ) (hk0 : (0 : ℝ) < k)
…

Mentions: OAI.PolycyclicRecognition.generatorSchemeWord, OAI.PolycyclicRecognition.generatorGroupWord