InverseTransferIdentity.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The actual inverse-coefficient transfer

The inverse transfer is the negative inverse linear map applied to the whole-fiber average. Its cocycle identity holds almost everywhere for each fixed group element, exactly as required for an L² cocycle.

def OAI.PolycyclicRecognition.inverseTheta line 26
Source documentation
The inverse-section transfer with its required inverse linear coefficient.
```
def inverseTheta (β : Measure G) (A : W ≃L[ℝ] W)
    (π l : G →* Multiplicative W) (φ : NormalizedPair G Λ → W)
    (p : NormalizedPair G Λ) : W := -A.symm (inverseAveragedTransfer β π l φ p)
…
```
Mentions: OAI.PolycyclicRecognition.NormalizedPair, OAI.PolycyclicRecognition.inverseAveragedTransfer

theorem OAI.PolycyclicRecognition.inverseTheta_memLp line 32

Source documentation

The constructed inverse transfer belongs to the actual L² space.

theorem inverseTheta_memLp
    (m : Measure G) [IsFiniteMeasureOnCompacts m]
    (μ ν : Measure (NormalizedPair G Λ)) [IsFiniteMeasure μ] [IsFiniteMeasure ν]
    (hprod : inversePairCoupling m μ = ν.prod m)
    (A : W ≃L[ℝ] W) (π 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 (inverseTheta (normalizedRestriction m B) A π l φ) 2 ν :=
…

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

theorem OAI.PolycyclicRecognition.inverseTheta_identity_ae line 46

Source documentation

The inverse transfer identity is derived on almost every fiber, with no assertion of a simultaneous exceptional set for all group elements.

theorem inverseTheta_identity_ae
    (m : Measure G) [IsFiniteMeasureOnCompacts m]
    (μ ν : Measure (NormalizedPair G Λ)) [IsFiniteMeasure μ] [IsFiniteMeasure ν]
    [SMulInvariantMeasure G (NormalizedPair G Λ) ν]
    (hprod : inversePairCoupling m μ = ν.prod m)
    (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φ : MemLp φ 2 μ)
    {B : Set G} (hB : IsCompact B) (hB0 : m B ≠ 0) (y : G) :
    ∀ᵐ p ∂ν, pairHeight π y p +
      inverseTheta (normalizedRestriction m B) A π l φ (normalizedTranslate y p) -
…

Mentions: OAI.PolycyclicRecognition.NormalizedPair, OAI.PolycyclicRecognition.inversePairCoupling, OAI.PolycyclicRecognition.pairHeight, OAI.PolycyclicRecognition.inverseTheta, OAI.PolycyclicRecognition.normalizedRestriction, OAI.PolycyclicRecognition.normalizedTranslate

def OAI.PolycyclicRecognition.inverseCocycleError line 73
Source documentation
The actual inverse-height cocycle after adding the inverse transfer.
```
def inverseCocycleError (β : Measure G) (A : W ≃L[ℝ] W)
    (π l : G →* Multiplicative W) (φ : NormalizedPair G Λ → W)
    (y : G) (p : NormalizedPair G Λ) : W :=
…
```
Mentions: OAI.PolycyclicRecognition.NormalizedPair

theorem OAI.PolycyclicRecognition.inverseCocycleError_lintegral_le line 81

Source documentation

Squared inverse-cocycle errors have at most the squared operator norm loss when compared with the averaged fiber error.

theorem inverseCocycleError_lintegral_le
    (m : Measure G) [IsFiniteMeasureOnCompacts m]
    (μ ν : Measure (NormalizedPair G Λ)) [IsFiniteMeasure μ] [IsFiniteMeasure ν]
    [SMulInvariantMeasure G (NormalizedPair G Λ) ν]
    (hprod : inversePairCoupling m μ = ν.prod m)
    (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φ : MemLp φ 2 μ)
    {B : Set G} (hB : IsCompact B) (hB0 : m B ≠ 0) (y : G) :
    (∫⁻ p, ‖inverseCocycleError (normalizedRestriction m B) A π l φ y p‖ₑ ^ 2 ∂ν) ≤
      ENNReal.ofReal ‖A.symm.toContinuousLinearMap‖ ^ 2 *
…

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

theorem OAI.PolycyclicRecognition.inverseCocycleError_tendsto_uniform line 122

Source documentation

Compact-uniform vanishing of averaged fiber errors gives the same vanishing for the actual inverse-coefficient cocycle.

theorem inverseCocycleError_tendsto_uniform
    (m : Measure G) [IsFiniteMeasureOnCompacts m]
    (μ ν : Measure (NormalizedPair G Λ)) [IsFiniteMeasure μ] [IsFiniteMeasure ν]
    [SMulInvariantMeasure G (NormalizedPair G Λ) ν]
    (hprod : inversePairCoupling m μ = ν.prod m)
    (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 μ)
    {B Q : Set G} (hB : IsCompact B) (hB0 : m B ≠ 0)
    (hR : Filter.Tendsto (fun n => ⨆ y ∈ Q,
      ∫⁻ p, ‖inverseAverageError (normalizedRestriction m B) π l (φ n) y p‖ₑ ^ 2 ∂ν)
…

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