InverseAverageL2.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The inverse transfer belongs to L²

The transfer in inverse coordinates is averaged over an actual positive compact Haar region. Local L² integrability and Jensen's estimate justify this construction for the finite inverse-section measure.

theorem OAI.PolycyclicRecognition.inverseFiberTransfer_memLp_normalized line 29

Source documentation

The corrected inverse transfer is square integrable on a normalized compact fiber region.

theorem inverseFiberTransfer_memLp_normalized
    (m : Measure G) [IsFiniteMeasureOnCompacts m]
    (μ ν : Measure (NormalizedPair G Λ)) [IsFiniteMeasure μ] [IsFiniteMeasure ν]
    (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 μ)
    {B : Set G} (hB : IsCompact B) (hB0 : m B ≠ 0) :
    MemLp (inverseFiberTransfer π l φ) 2 (ν.prod (normalizedRestriction m B)) := by
…

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

theorem OAI.PolycyclicRecognition.inverseFiberTransfer_shift_memLp line 46

Source documentation

Translating the compact fiber region by its evaluation center retains square integrability. Stationarity handles the normalized section shift.

theorem inverseFiberTransfer_shift_memLp
    (ν : Measure (NormalizedPair G Λ)) [IsFiniteMeasure ν]
    [SMulInvariantMeasure G (NormalizedPair G Λ) ν]
    (β : Measure G) [IsProbabilityMeasure β]
    (π l : G →* Multiplicative W) (hl : Continuous fun g => (l g).toAdd)
    (φ : NormalizedPair G Λ → W)
    (hD : MemLp (inverseFiberTransfer π l φ) 2 (ν.prod β)) (y : G) :
    MemLp (fun q : NormalizedPair G Λ × G =>
      inverseFiberTransfer π l φ (q.1, q.1.val.1 y * q.2)) 2 (ν.prod β) := by
…

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

theorem OAI.PolycyclicRecognition.inverseAveragedTransfer_memLp line 80

Source documentation

The averaged inverse transfer is an actual square-integrable function for the section measure constructed by Haar factorization.

theorem inverseAveragedTransfer_memLp
    (m : Measure G) [IsFiniteMeasureOnCompacts m]
    (μ ν : Measure (NormalizedPair G Λ)) [IsFiniteMeasure μ] [IsFiniteMeasure ν]
    (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 μ)
    {B : Set G} (hB : IsCompact B) (hB0 : m B ≠ 0) :
    MemLp (inverseAveragedTransfer (normalizedRestriction m B) π l φ) 2 ν := by
…

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

theorem OAI.PolycyclicRecognition.inverseAverageError_sq_le line 98

Source documentation

For two square-integrable fiber restrictions, the average error is bounded by their whole-product squared oscillation.

theorem inverseAverageError_sq_le
    (β : Measure G) [IsProbabilityMeasure β]
    (π l : G →* Multiplicative W) (φ : NormalizedPair G Λ → W)
    (y : G) (p : NormalizedPair G Λ)
    (h₁ : MemLp (fun x => inverseFiberTransfer π l φ (p, p.val.1 y * x)) 2 β)
    (h₂ : MemLp (fun x => inverseFiberTransfer π l φ (p, x)) 2 β) :
    ‖inverseAverageError β π l φ y p‖ ^ 2 ≤
      ∫ x₁, ∫ x₂, ‖pairTransferDefect π l φ (x₂⁻¹ * (p.val.1 y * x₁))
        (pairChartTransition.symm (p, x₂)).2‖ ^ 2 ∂β ∂β := by
…

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

theorem OAI.PolycyclicRecognition.inverse_transfer_linear_coefficient line 116
Source documentation
Algebraic final step of the inverse transfer: the linear coefficient is precisely the inverse of the original coefficient.
```
theorem inverse_transfer_linear_coefficient (A : W ≃L[ℝ] W)
    {v w ψ ψ' R : W} (h : ψ' - ψ = -v + A w + R) :
    w + (-A.symm ψ') - (-A.symm ψ) = A.symm v - A.symm R := by
…
```