OAI/Dynamics/ThreeTorus/Whitening.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ThreeTorus.energyWeight line 20

   Source documentation

   Squared modulus as a nonnegative measure density.

   def energyWeight {X : Type*} (F : X → ℂ) (x : X) : ℝ≥0∞ :=
   …

2. lemma OAI.ThreeTorus.measurable_energyWeight line 23
3. lemma OAI.ThreeTorus.energyWeight_mul line 27
4. lemma OAI.ThreeTorus.energy_map_multiplier line 35

   Source documentation

   Spectral multipliers act by multiplying the pushforward energy density.

   lemma energy_map_multiplier {X Y : Type*} [MeasurableSpace X] [MeasurableSpace Y]
       {μ : Measure X} {ν : Measure Y} {ζ : X → Y} {F : X → ℂ} {p : Y → ℝ≥0∞}
       (hζ : Measurable ζ) (hF : Measurable F) (hp : Measurable p)
       (hpush : (μ.withDensity (energyWeight F)).map ζ = ν.withDensity p)
       {a : Y → ℂ} (ha : Measurable a) :
       (μ.withDensity (energyWeight (fun x => a (ζ x) * F x))).map ζ =
         ν.withDensity (p * energyWeight a) := by
   …

   Mentions: OAI.ThreeTorus.μ, OAI.ThreeTorus.energyWeight

5. lemma OAI.ThreeTorus.energy_zero_fiber line 50

   Source documentation

   A coefficient is zero almost everywhere over the zero set of its spectral density.

   lemma energy_zero_fiber {X Y : Type*} [MeasurableSpace X] [MeasurableSpace Y]
       {μ : Measure X} {ν : Measure Y} {ζ : X → Y} {F : X → ℂ} {p : Y → ℝ}
       (hζ : Measurable ζ) (hF : Measurable F) (hp : Measurable p)
       (hpush : (μ.withDensity (energyWeight F)).map ζ =
         ν.withDensity (fun y => ENNReal.ofReal (p y))) :
       ∀ᵐ x ∂μ, p (ζ x) = 0 → F x = 0 := by
   …

   Mentions: OAI.ThreeTorus.μ, OAI.ThreeTorus.energyWeight

6. def OAI.ThreeTorus.whitenCoefficient line 72

   Source documentation

   The exact whitening coefficient, filling the density's zero set with a flat vector.

   def whitenCoefficient {X Y : Type*} (ζ : X → Y) (p : Y → ℝ)
       (F V : X → ℂ) (x : X) : ℂ :=
   …

7. lemma OAI.ThreeTorus.measurable_whitenCoefficient line 76
8. lemma OAI.ThreeTorus.whiten_reconstruct line 83
9. lemma OAI.ThreeTorus.energy_map_piecewise line 100

   Source documentation

   A piecewise multiplier rule: the two spectral supports can overlap in angular index; it is their frequency supports that are disjoint.

   lemma energy_map_piecewise {X Y : Type*} [MeasurableSpace X] [MeasurableSpace Y]
       {μ : Measure X} {ν : Measure Y} {ζ : X → Y} {F V : X → ℂ}
       {p q : Y → ℝ≥0∞} {s : Set Y}
       (hζ : Measurable ζ) (hF : Measurable F) (hV : Measurable V)
       (hp : Measurable p) (hq : Measurable q) (hs : MeasurableSet s)
       (hpushF : (μ.withDensity (energyWeight F)).map ζ = ν.withDensity p)
       (hpushV : (μ.withDensity (energyWeight V)).map ζ = ν.withDensity q)
       {a b : Y → ℂ} (ha : Measurable a) (hb : Measurable b) :
       (μ.withDensity (energyWeight (fun x => if ζ x ∈ s then a (ζ x) * F x
         else b (ζ x) * V x))).map ζ =
         ν.withDensity (fun y => if y ∈ s then p y * energyWeight a y
           else q y * energyWeight b y) := by
   …

   Mentions: OAI.ThreeTorus.μ, OAI.ThreeTorus.energyWeight

10. lemma OAI.ThreeTorus.positive_whitening_weight line 130
11. lemma OAI.ThreeTorus.whiten_energy_map line 139

    Source documentation

    Exact flat output intensity, including the zero set, without requiring angular supports of the two coefficient families to be disjoint.

    lemma whiten_energy_map {X Y : Type*} [MeasurableSpace X] [MeasurableSpace Y]
        {μ : Measure X} {ν : Measure Y} {ζ : X → Y} {F V : X → ℂ} {p : Y → ℝ}
        (hζ : Measurable ζ) (hF : Measurable F) (hV : Measurable V)
        (hp : Measurable p) (hpn : ∀ y, 0 ≤ p y)
        (hpush : (μ.withDensity (energyWeight F)).map ζ =
          ν.withDensity (fun y => ENNReal.ofReal (p y)))
        (hflat : (μ.withDensity (energyWeight V)).map ζ = ν) :
        (μ.withDensity (energyWeight (whitenCoefficient ζ p F V))).map ζ = ν := by
    …

    Mentions: OAI.ThreeTorus.μ, OAI.ThreeTorus.energyWeight, OAI.ThreeTorus.whitenCoefficient

12. lemma OAI.ThreeTorus.whitening_scalar_distance line 174
13. lemma OAI.ThreeTorus.whiten_error_energy_map line 185

    Source documentation

    The error's entire spectral density, not just its total mass, is exactly (√p - 1)². This entails the source's whitening-distance identity.

    lemma whiten_error_energy_map {X Y : Type*} [MeasurableSpace X] [MeasurableSpace Y]
        {μ : Measure X} {ν : Measure Y} {ζ : X → Y} {F V : X → ℂ} {p : Y → ℝ}
        (hζ : Measurable ζ) (hF : Measurable F) (hV : Measurable V)
        (hp : Measurable p) (hpn : ∀ y, 0 ≤ p y)
        (hpush : (μ.withDensity (energyWeight F)).map ζ =
          ν.withDensity (fun y => ENNReal.ofReal (p y)))
        (hflat : (μ.withDensity (energyWeight V)).map ζ = ν) :
        (μ.withDensity (energyWeight (fun x => whitenCoefficient ζ p F V x - F x))).map ζ =
          ν.withDensity (fun y => ENNReal.ofReal ((Real.sqrt (p y) - 1) ^ 2)) := by
    …

    Mentions: OAI.ThreeTorus.μ, OAI.ThreeTorus.energyWeight, OAI.ThreeTorus.whitenCoefficient

14. lemma OAI.ThreeTorus.energy_map_total line 224
15. lemma OAI.ThreeTorus.whiten_memLp line 235

    Source documentation

    The whitened coefficient really belongs to L² whenever the spectral reference measure is finite; its possible singular multiplier does not obstruct this.

    lemma whiten_memLp {X Y : Type*} [MeasurableSpace X] [MeasurableSpace Y]
        {μ : Measure X} {ν : Measure Y} [IsFiniteMeasure ν]
        {ζ : X → Y} {F V : X → ℂ} {p : Y → ℝ}
        (hζ : Measurable ζ) (hF : Measurable F) (hV : Measurable V)
        (hp : Measurable p) (hpn : ∀ y, 0 ≤ p y)
        (hpush : (μ.withDensity (energyWeight F)).map ζ =
          ν.withDensity (fun y => ENNReal.ofReal (p y)))
        (hflat : (μ.withDensity (energyWeight V)).map ζ = ν) :
        MemLp (whitenCoefficient ζ p F V) 2 μ := by
    …

    Mentions: OAI.ThreeTorus.μ, OAI.ThreeTorus.energyWeight, OAI.ThreeTorus.whitenCoefficient

16. lemma OAI.ThreeTorus.whiten_distance_integral line 256