OAI/Analysis/LipschitzHilbert/Trees/SourcePlanarSynthesis.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Finite sums of the original scalar planar packets are actual vector Schwartz maps, and their coordinate cutoffs follow from those of the nonzero summands.

  1. def OAI.LipschitzHilbert.planarSynthesisSchwartz line 16

    Source documentation

    The Schwartz-map representative of the manuscript's fixed synthesis.

    def planarSynthesisSchwartz (c : ι → EuclideanSpace ℂ κ)
    (f : ι → κ → SchwartzMap (ℝ×ℝ) ℂ) : SchwartzMap (ℝ×ℝ) (EuclideanSpace ℂ κ) :=
…
  2. theorem OAI.LipschitzHilbert.planarSynthesisSchwartz_apply line 20
  3. theorem OAI.LipschitzHilbert.planarSynthesisSchwartz_horizontal line 27
  4. theorem OAI.LipschitzHilbert.planarSynthesisSchwartz_vertical line 36
  5. theorem OAI.LipschitzHilbert.planarSynthesisSchwartz_coordinate_bands line 45