SourceTreeDensityTerm.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

A single short-tree term is controlled by its actual density test. Extra packet decay retains the distance to the horizontal strip.

theorem OAI.LipschitzHilbert.taxicab_quadratic_le line 15
theorem OAI.LipschitzHilbert.packet_envelope_density_decay line 26
Source documentation
The physical product envelope dominates the density kernel, while leaving any prescribed number of horizontal decay powers.
```
theorem packet_envelope_density_decay (T : SlopeBox) (D r : ℕ) (z : ℝ×ℝ) :
    lineEnvelope T.x T.length (D+r) z.1 *
      lineEnvelope (T.y-T.slope*T.x) T.width (D+r) (z.2-T.slope*z.1) ≤
      3^D*T.densityKernel D z*lineEnvelope T.x T.length r z.1 := by
…
```
Mentions: OAI.LipschitzHilbert.SlopeBox, OAI.LipschitzHilbert.lineEnvelope
theorem OAI.LipschitzHilbert.horizontal_envelope_le_distance line 70

theorem OAI.LipschitzHilbert.OrdinaryDensityTile.test_integral_le_density line 87

Source documentation

Every admissible test is bounded by the literal density supremum.

theorem test_integral_le_density (tile : OrdinaryDensityTile)
    (ell0 w W tau : ℝ) (grid : ℤ) (E : Set (ℝ×ℝ)) (v : ℝ×ℝ → ℝ)
    (test : OrdinaryDensityTest ell0 w W tau grid tile) :
    (∫ z in E ∩ v ⁻¹' scaledAngularCell (w/ell0) grid test.level test.cell,
      test.top.densityKernel 203 z ∂volume.prod volume) ≤
        tile.density ell0 w W tau grid E v*test.top.area := by
…

Mentions: OAI.LipschitzHilbert.OrdinaryDensityTile, OAI.LipschitzHilbert.OrdinaryDensityTest, OAI.LipschitzHilbert.scaledAngularCell

theorem OAI.LipschitzHilbert.density_test_short_packet_term line 102

Source documentation

One literal physical packet term. Its selector may be complex and coordinate-dependent; only its original support and norm bound are used.

theorem density_test_short_packet_term {κ : Type} [Fintype κ]
    (ell0 w W tau : ℝ) (grid : ℤ) (tile : OrdinaryDensityTile)
    (test : OrdinaryDensityTest ell0 w W tau grid tile)
    (r n : ℕ) (horder : 203+r≤n) (C M sigma eta d : ℝ)
    (hC : 0≤C) (hM : 0≤M) (hsigma : 0≤sigma) (hd : 0≤d)
    (profile : κ → SchwartzMap (ℝ×ℝ) ℂ) (frequency : κ → ℝ)
    (hprofile : ∀ k, planarProfileConstant (profile k) n≤C)
    (c : EuclideanSpace ℂ κ) (hc : ‖c‖≤sigma)
    (selector : κ → ℝ → ℂ) (hselector : ∀ k, Measurable (selector k))
    (hbound : ∀ k s, ‖selector k s‖≤M)
    (hsupport : ∀ k s, selector k s≠0 →
      s∈scaledAngularCell (w/ell0) grid test.level test.cell)
…

Mentions: OAI.LipschitzHilbert.OrdinaryDensityTile, OAI.LipschitzHilbert.OrdinaryDensityTest, OAI.LipschitzHilbert.planarProfileConstant, OAI.LipschitzHilbert.scaledAngularCell