OAI/Analysis/LipschitzHilbert/Trees/SourceVerticalDemodulation.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LipschitzHilbert.verticalCarrier line 16
2. theorem OAI.LipschitzHilbert.verticalCarrier_temperate line 18
3. theorem OAI.LipschitzHilbert.verticalCarrier_norm line 22
4. def OAI.LipschitzHilbert.verticalDemodulation line 25
5. theorem OAI.LipschitzHilbert.verticalDemodulation_apply line 31
6. theorem OAI.LipschitzHilbert.verticalDemodulation_norm line 38
7. def OAI.LipschitzHilbert.scalarVerticalDemodulation line 46
8. theorem OAI.LipschitzHilbert.scalarVerticalDemodulation_apply line 50
9. theorem OAI.LipschitzHilbert.verticalDemodulation_zero line 55
10. theorem OAI.LipschitzHilbert.verticalDemodulation_sub line 60
11. theorem OAI.LipschitzHilbert.verticalDemodulation_sum line 66
12. theorem OAI.LipschitzHilbert.demodulated_family_box_bound line 74

    Source documentation

    Uniform box control uses the demodulated supports, so its constants are independent of the location of the individual vertical carriers.

    theorem demodulated_family_box_bound {ι : Type*}
        (Kx Ky : SchwartzMap ℝ ℂ) (nu : κ → ℝ)
        (F : ι → SchwartzMap (ℝ×ℝ) (EuclideanSpace ℂ κ))
        (Rx Ry cx cy rx ry : ℝ) (hrx : 0<rx) (hry : 0<ry)
        (hKx : ∀ ξ, |ξ|≤Rx → 𝓕 Kx ξ=1) (hKy : ∀ η, |η|≤Ry → 𝓕 Ky η=1)
        (hFx : ∀ a y ξ, 𝓕 (vectorHorizontalSlice (verticalDemodulation nu (F a)) y) ξ≠0 → |ξ|≤Rx/rx)
        (hFy : ∀ a x η, 𝓕 (vectorVerticalSlice (verticalDemodulation nu (F a)) x) η≠0 → |η|≤Ry/ry)
        (U : ℝ×ℝ → ℝ) (hUm : Measurable U) (hU2 : MemLp U 2 (volume.prod volume))
        (B : ℝ) (hB : 0≤B) (hU0 : ∀ p, 0≤U p) (hUb : ∀ p, ‖U p‖≤B)
        (hFU : ∀ a p, ‖F a p‖≤U p) :
        ∀ᵐ z ∂volume.prod volume, z∈coordinateBox cx cy rx ry →
          ∀ a w, w∈coordinateBox cx cy rx ry →
    …

    Mentions: OAI.LipschitzHilbert.vectorHorizontalSlice, OAI.LipschitzHilbert.verticalDemodulation, OAI.LipschitzHilbert.vectorVerticalSlice, OAI.LipschitzHilbert.coordinateBox