InverseDefectControl.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Controlling inverse oscillations by the original defects

This is the compact-region estimate in the inverse-coupling argument. All three integrations are over whole fibers. Their bound is a fixed product of Haar masses times the original section error.

theorem OAI.PolycyclicRecognition.measurable_pairTransferDefect line 27

Source documentation

Joint measurability of the actual stationary coboundary defect.

theorem measurable_pairTransferDefect (π l : G →* Multiplicative W)
    (hπ : Continuous fun g => (π g).toAdd) (hl : Continuous fun g => (l g).toAdd)
    {φ : NormalizedPair G Λ → W} (hφ : Measurable φ) :
    Measurable (fun q : G × NormalizedPair G Λ => pairTransferDefect π l φ q.1 q.2) := by
…

Mentions: OAI.PolycyclicRecognition.NormalizedPair, OAI.PolycyclicRecognition.pairTransferDefect

theorem OAI.PolycyclicRecognition.inverse_defect_oscillation_bound line 43

Source documentation

The inverse oscillation integral over bounded regions is bounded by the original section defect, with constants independent of the translating center.

theorem inverse_defect_oscillation_bound
    (m : Measure G) [SFinite m] [m.IsMulLeftInvariant]
    (μ ν : Measure (NormalizedPair G Λ)) [SFinite μ] [SFinite ν]
    (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φ : Measurable φ)
    {B C T : Set G} (hB : MeasurableSet B) (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∞}
    (hc : ∀ t ∈ T, (∫⁻ p, ‖pairTransferDefect π l φ t p‖ₑ ^ 2 ∂μ) ≤ c) :
…

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