CouplingLocalL2.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Local square integrability of the coupling transfers

A square-integrable section transfer becomes locally square integrable after adding the continuous target height. This property is preserved by the actual change to inverse coordinates.

theorem OAI.PolycyclicRecognition.pairTransferLift_memLp_compact line 30

Source documentation

The lifted transfer is square integrable on every compact subset of the first product chart.

theorem pairTransferLift_memLp_compact
    (m : Measure G) [IsFiniteMeasureOnCompacts m]
    (μ : Measure (NormalizedPair G Λ)) [IsFiniteMeasure μ]
    (π : G →* Multiplicative W) (hπ : Continuous fun g => (π g).toAdd)
    {φ : NormalizedPair G Λ → W} (hφ : MemLp φ 2 μ)
    {K : Set (G × NormalizedPair G Λ)} (hK : IsCompact K) :
    MemLp (pairTransferLift π φ) 2 ((m.prod μ).restrict K) := by
…

Mentions: OAI.PolycyclicRecognition.NormalizedPair, OAI.PolycyclicRecognition.pairTransferLift

theorem OAI.PolycyclicRecognition.inverseFiberTransfer_memLp_compact line 55

Source documentation

The corrected transfer in the inverse chart is locally square integrable for the coupling measure.

theorem inverseFiberTransfer_memLp_compact
    (m : Measure G) [IsFiniteMeasureOnCompacts m]
    (μ : Measure (NormalizedPair G Λ)) [IsFiniteMeasure μ]
    (π l : G →* Multiplicative W)
    (hπ : Continuous fun g => (π g).toAdd) (hl : Continuous fun g => (l g).toAdd)
    {φ : NormalizedPair G Λ → W} (hφ : MemLp φ 2 μ)
    {K : Set (NormalizedPair G Λ × G)} (hK : IsCompact K) :
    MemLp (inverseFiberTransfer π l φ) 2 ((inversePairCoupling m μ).restrict K) := by
…

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