InverseCompactControl.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Compact regions in the inverse coupling

A compact family of evaluation points yields common compact averaging and increment regions. Integrals on an inverse-chart strip are bounded by a fixed Haar mass times the original section integral.

theorem OAI.PolycyclicRecognition.exists_inverse_compact_regions line 26

Source documentation

Uniform compact regions for the centers, their translated averaging regions, and the resulting difference parameters.

theorem exists_inverse_compact_regions {Q B : Set G} (hQ : IsCompact Q) (hB : IsCompact B) :
    ∃ C T : Set G, IsCompact C ∧ IsCompact T ∧
      (∀ y ∈ Q, ∀ p : NormalizedPair G Λ, ∀ x ∈ B, p.val.1 y * x ∈ C) ∧
      (∀ x₂ ∈ B, ∀ x₁ ∈ C, x₂⁻¹ * x₁ ∈ T) := by
…

Mentions: OAI.PolycyclicRecognition.NormalizedPair

def OAI.PolycyclicRecognition.inverseStripBase line 42
Source documentation
The first-coordinate projection of a compact strip in inverse coordinates. Its Haar mass is the constant in the local error bound.
```
def inverseStripBase (B : Set G) : Set G :=
…
```
theorem OAI.PolycyclicRecognition.inverseStripBase_compact line 45

theorem OAI.PolycyclicRecognition.inverse_strip_lintegral_le line 54

Source documentation

Product coordinates bound every inverse-strip integral by the Haar mass of one compact base projection times its section integral.

theorem inverse_strip_lintegral_le
    (m : Measure G) [SFinite m]
    (μ ν : Measure (NormalizedPair G Λ)) [SFinite μ] [SFinite ν]
    (hprod : inversePairCoupling m μ = ν.prod m)
    (B : Set G) (f : NormalizedPair G Λ → ℝ≥0∞) (hf : Measurable f) :
    (∫⁻ p, ∫⁻ x in B, f (pairChartTransition.symm (p, x)).2 ∂m ∂ν) ≤
      m (inverseStripBase (Λ := Λ) B) * ∫⁻ p, f p ∂μ := by
…

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