OAI/Analysis/LipschitzHilbert/Trees/SourceGramMargin.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The fixed angular margin of an actual packet transfers to every direction sufficiently close to its slope, using a common Fourier witness.

  1. theorem OAI.LipschitzHilbert.frequency_slope_distance line 11
  2. theorem OAI.LipschitzHilbert.gram_margin_direction_mem line 31

    Source documentation

    This uses the manuscript's support margin, not an assumed angular membership for the direction that will be used in deletion.

    theorem gram_margin_direction_mem (f g : SchwartzMap (ℝ×ℝ) ℂ)
    (theta ell w cStar cEta margin u : ℝ) (omega : Set ℝ)
    (hell : 0<ell) (hw : 0<w) (hcEta : 0<cEta)
    (hf : ∀ xi eta, planarAngularFourier f (xi,eta)≠0 →
      |xi+theta*eta|≤cStar/ell ∧ cEta≤w*eta)
    (hmargin : ∀ xi eta, planarAngularFourier f (xi,eta)≠0 →
      Icc (-xi/eta-margin*(w/ell)) (-xi/eta+margin*(w/ell))⊆omega)
    (hu : |u-theta|≤(margin-cStar/cEta)*(w/ell))
    (hinner : (∫ z, inner ℂ (f z) (g z) ∂volume.prod volume)≠0) : u∈omega := by
…

    Mentions: OAI.LipschitzHilbert.planarAngularFourier