OAI/Analysis/LipschitzHilbert/Trees/SourceVectorReproduction.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LipschitzHilbert.vector_schwartz_convolution_reproduction line 16

   Source documentation

   Scalar convolution reproduces a vector Schwartz function on its original Fourier support.

   theorem vector_schwartz_convolution_reproduction
       (K : SchwartzMap ℝ ℂ) (f : SchwartzMap ℝ (EuclideanSpace ℂ κ))
       (hK : ∀ ξ, 𝓕 f ξ≠0 → 𝓕 K ξ=1) :
       SchwartzMap.convolution (ContinuousLinearMap.lsmul ℂ ℂ) K f=f := by
   …

2. theorem OAI.LipschitzHilbert.vector_schwartz_integral_reproduction line 34

   Source documentation

   The symmetric integral formula places the packet norm under a positive scalar kernel.

   theorem vector_schwartz_integral_reproduction
       (K : SchwartzMap ℝ ℂ) (f : SchwartzMap ℝ (EuclideanSpace ℂ κ))
       (hK : ∀ ξ, 𝓕 f ξ≠0 → 𝓕 K ξ=1) (x : ℝ) :
       f x=∫ y, K (x-y) • f y := by
   …

3. theorem OAI.LipschitzHilbert.vector_family_reproduction_bound line 46

   Source documentation

   Uniform local reproduction for every member of a vector family, from one common scalar norm majorant. The null set is common to the whole family and to all spatial evaluation points.

   theorem vector_family_reproduction_bound {ι : Type*}
       (K : SchwartzMap ℝ ℂ) (R : ℝ) (r : ι → ℝ) (hr : ∀ a, 0<r a)
       (hK : ∀ ξ, |ξ|≤R → 𝓕 K ξ=1)
       (F : ι → SchwartzMap ℝ (EuclideanSpace ℂ κ))
       (hfreq : ∀ a ξ, 𝓕 (F a) ξ≠0 → |ξ|≤R/(r a))
       (U : ℝ → ℝ) (hUm : Measurable U) (hU2 : MemLp U 2 volume)
       (hU0 : ∀ x, 0≤U x) (B : ℝ) (hUb : ∀ x, ‖U x‖≤B)
       (hFU : ∀ a x, ‖F a x‖≤U x) :
       ∀ᵐ z ∂volume, ∀ a x, |x-z|≤r a →
         ‖F a x‖≤(96*schwartzEnvelopeConstant K 1)*DyadicLineGrid.threeGridMaximal U z := by
   …

   Mentions: OAI.LipschitzHilbert.schwartzEnvelopeConstant, OAI.LipschitzHilbert.DyadicLineGrid.threeGridMaximal