UniformBoxTranslation.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform small translations of actual model cells

theorem OAI.PolycyclicRecognition.model_cell_boundary_loss_tendstoUniformly line 23

Source documentation

A common vanishing normalized coordinate bound gives uniform boundary loss in every sampled parameter. No convergence of the basis is required.

theorem model_cell_boundary_loss_tendstoUniformly
    (haar : NilpotentExponentialHaarInput E G)
    (Exp : GroupLieAlgebra (𝓘(ℝ, E)) G → G) (hExp : IsGroupExponential Exp)
    (e : L ≃ₗ⁅ℝ⁆ GroupLieAlgebra (𝓘(ℝ, E)) G)
    (hnil : LieRing.IsNilpotent (GroupLieAlgebra (𝓘(ℝ, E)) G))
    {n c : ℕ} (b : ι → Basis (Fin n) ℝ L)
    (a : DynkinCoefficients c 2)
    (hm : ∀ x y, Exp (finiteDynkinPolynomial a ![x, y]) = Exp x * Exp y)
    {C : ℝ} (hbound : ∀ i, ‖basisBracket (b i)‖ ≤ C)
    {l : Filter ι} (q : ι → Z → Fin n → ℝ)
    (hq : TendstoUniformly q (fun _ => 0) l)
    {S : Set (Fin n → ℝ)} (hS : MeasurableSet S) (hfin : volume S ≠ ⊤) :
…

Mentions: OAI.PolycyclicRecognition.NilpotentExponentialHaarInput, OAI.PolycyclicRecognition.DynkinCoefficients, OAI.PolycyclicRecognition.finiteDynkinPolynomial, OAI.PolycyclicRecognition.basisBracket

theorem OAI.PolycyclicRecognition.model_cell_observable_error_tendstoUniformly line 50

Source documentation

Uniformity also holds after projection to any bounded observable, even when that observable depends on the scale and the sampled parameter.

theorem model_cell_observable_error_tendstoUniformly
    (haar : NilpotentExponentialHaarInput E G)
    (Exp : GroupLieAlgebra (𝓘(ℝ, E)) G → G) (hExp : IsGroupExponential Exp)
    (e : L ≃ₗ⁅ℝ⁆ GroupLieAlgebra (𝓘(ℝ, E)) G)
    (hnil : LieRing.IsNilpotent (GroupLieAlgebra (𝓘(ℝ, E)) G))
    {n c : ℕ} (b : ι → Basis (Fin n) ℝ L)
    (a : DynkinCoefficients c 2)
    (hm : ∀ x y, Exp (finiteDynkinPolynomial a ![x, y]) = Exp x * Exp y)
    {C : ℝ} (hbound : ∀ i, ‖basisBracket (b i)‖ ≤ C)
    {l : Filter ι} (q : ι → Z → Fin n → ℝ)
    (hq : TendstoUniformly q (fun _ => 0) l)
    {S : Set (Fin n → ℝ)} (hS : MeasurableSet S) (hfin : volume S ≠ ⊤)
…