InverseErrorBound.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The normalized inverse-transfer error bound

The actual error of the averaged inverse transfer is controlled by the original stationary defect on one compact increment region. Every factor in the bound is independent of the chosen evaluation point in that region.

theorem OAI.PolycyclicRecognition.inverseAverageError_lintegral_le line 29

Source documentation

Quantitative whole-fiber estimate for the actual averaged inverse error. The original defect bound is used only on the displayed increment set.

theorem inverseAverageError_lintegral_le
    (m : Measure G) [m.IsHaarMeasure]
    (μ ν : Measure (NormalizedPair G Λ)) [IsFiniteMeasure μ] [IsFiniteMeasure ν]
    [SMulInvariantMeasure G (NormalizedPair G Λ) ν]
    (hprod : inversePairCoupling m μ = ν.prod m)
    (π l : G →* Multiplicative W)
    (hπ : Continuous fun g => (π g).toAdd) (hl : Continuous fun g => (l g).toAdd)
    {φ : NormalizedPair G Λ → W} (hφ : MemLp φ 2 μ) (hφm : Measurable φ)
    {B C T : Set G} (hB : IsCompact B) (hB0 : m B ≠ 0) (hTm : MeasurableSet T)
    (hT : ∀ x₂ ∈ B, ∀ x₁ ∈ C, x₂⁻¹ * x₁ ∈ T)
    (y : G) (hC : ∀ p : NormalizedPair G Λ, ∀ x ∈ B, p.val.1 y * x ∈ C)
    {c : ℝ≥0∞}
…

Mentions: OAI.PolycyclicRecognition.NormalizedPair, OAI.PolycyclicRecognition.inversePairCoupling

theorem OAI.PolycyclicRecognition.inverseAverageError_tendsto_uniform line 58

Source documentation

Compact-uniform vanishing of the original defects implies uniform vanishing of the squared inverse-average errors on the chosen region.

theorem inverseAverageError_tendsto_uniform
    (m : Measure G) [m.IsHaarMeasure]
    (μ ν : Measure (NormalizedPair G Λ)) [IsFiniteMeasure μ] [IsFiniteMeasure ν]
    [SMulInvariantMeasure G (NormalizedPair G Λ) ν]
    (hprod : inversePairCoupling m μ = ν.prod m)
    (π l : G →* Multiplicative W)
    (hπ : Continuous fun g => (π g).toAdd) (hl : Continuous fun g => (l g).toAdd)
    (φ : ℕ → NormalizedPair G Λ → W)
    (hφ : ∀ n, MemLp (φ n) 2 μ) (hφm : ∀ n, Measurable (φ n))
    {B C T Q : Set G} (hB : IsCompact B) (hB0 : m B ≠ 0) (hTc : IsCompact T)
    (hT : ∀ x₂ ∈ B, ∀ x₁ ∈ C, x₂⁻¹ * x₁ ∈ T)
    (hC : ∀ y ∈ Q, ∀ p : NormalizedPair G Λ, ∀ x ∈ B, p.val.1 y * x ∈ C)
…

Mentions: OAI.PolycyclicRecognition.NormalizedPair, OAI.PolycyclicRecognition.inversePairCoupling