SourceGramGeometry.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Actual nonzero Gram interactions force the angular proximity used in the selected-tree Bessel argument.

theorem OAI.LipschitzHilbert.common_wedge_distance line 11
theorem OAI.LipschitzHilbert.planar_packet_gram_angle line 31

theorem OAI.LipschitzHilbert.gram_short_direction line 46

Source documentation

A sufficiently longer interacting packet lies close to the longer tree's direction in units of the shorter packet's angular scale.

theorem gram_short_direction (f g : SchwartzMap (ℝ×ℝ) ℂ)
    (theta phi t ell r w cStar cEta CEta cOne COmega CZero : ℝ)
    (hell : 0<ell) (hr : 0<r) (hw : 0<w) (hcStar : 0≤cStar)
    (hcEta : 0<cEta) (hCOmega : 0≤COmega) (hCZero : 0<CZero)
    (hlong : CZero*ell≤r)
    (hconstants : (cStar/cEta)*(1+1/CZero)+COmega/CZero≤cOne/4)
    (htop : |phi-t|≤COmega*(w/r))
    (hf : ∀ xi eta, planarAngularFourier f (xi,eta)≠0 →
      |xi+theta*eta|≤cStar/ell ∧ cEta≤w*eta ∧ w*eta≤CEta)
    (hg : ∀ xi eta, planarAngularFourier g (xi,eta)≠0 →
      |xi+phi*eta|≤cStar/r ∧ cEta≤w*eta ∧ w*eta≤CEta)
    (hinner : (∫ z, inner ℂ (f z) (g z) ∂volume.prod volume)≠0) :
…

Mentions: OAI.LipschitzHilbert.planarAngularFourier

theorem OAI.LipschitzHilbert.selected_direction_order_contradiction line 77

Source documentation

The near-extremal direction rule rules out the wrong temporal order once these two geometric slope estimates hold.

theorem selected_direction_order_contradiction
    (theta t selected other d cOne epsilon : ℝ)
    (hd : 0<d) (hcOne : 0<cOne)
    (hnear : |theta-t|≤cOne*d/4)
    (hselected : theta+cOne*d≤selected)
    (hother : |other-t|≤cOne*d/4)
    (hepsilon : epsilon≤cOne*d/4)
    (hfirst : selected<other+epsilon) : False := by
…