SourceBoxReproduction.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Uniform reproduction on a physical rectangle. The two spectra are properties of the actual coordinate restrictions, and all vector members are controlled by one scalar maximal function.

def OAI.LipschitzHilbert.coordinateBox line 15
theorem OAI.LipschitzHilbert.coordinateBox_measurable line 18
theorem OAI.LipschitzHilbert.planar_reproduction_kernel_bound line 23

theorem OAI.LipschitzHilbert.planar_family_box_bound line 63

Source documentation

One exceptional set controls every packet and every evaluation point of the box.

theorem planar_family_box_bound {ι : Type*}
    (Kx Ky : SchwartzMap ℝ ℂ) (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 (F a) y) ξ≠0 → |ξ|≤Rx/rx)
    (hFy : ∀ a x η, 𝓕 (vectorVerticalSlice (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 →
        ‖F a w‖≤(147456*schwartzEnvelopeConstant Kx 1*schwartzEnvelopeConstant Ky 1)*
…

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