InverseCoupling.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Inverse coupling with the prescribed inverse coefficient

Compact-uniform approximation of the forward height cocycle transfers to the inverse section, with precisely the inverse linear coefficient. The measure and the square-integrable transfer functions are constructed from the pair-space charts and whole-fiber averages.

theorem OAI.PolycyclicRecognition.inverseCoupling line 30

Source documentation

The manuscript's inverse-coupling construction, in the equivalent squared-L² compact-uniform formulation. The inverse-section measure and all inverse transfer functions are produced by the proof.

theorem inverseCoupling
    (m : Measure G) [m.IsHaarMeasure] [m.IsMulRightInvariant]
    (μ : Measure (NormalizedPair G Λ)) [IsProbabilityMeasure μ]
    [SMulInvariantMeasure G (NormalizedPair G Λ) μ]
    (A : W ≃L[ℝ] W) (π l : G →* Multiplicative W)
    (hπ : Continuous fun g => (π g).toAdd) (hl : Continuous fun g => (l g).toAdd)
    (hlA : ∀ g, (l g).toAdd = A (π g).toAdd)
    (φ : ℕ → NormalizedPair G Λ → W)
    (hφ : ∀ n, MemLp (φ n) 2 μ) (hφm : ∀ n, Measurable (φ n))
    (happrox : ∀ T : Set G, IsCompact T →
      Filter.Tendsto (fun n => ⨆ t ∈ T,
        ∫⁻ p, ‖pairTransferDefect π l (φ n) t p‖ₑ ^ 2 ∂μ) Filter.atTop (nhds 0)) :
…

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