PacketDataDensity.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Own-box density and the short-packet estimate for unrestricted lattice slopes. Only the intrinsic two-dimensional profile is used.

abbrev OAI.LipschitzHilbert.PacketLatticeData.PacketIndex line 17
def OAI.LipschitzHilbert.PacketLatticeData.densityTile line 19
def OAI.LipschitzHilbert.PacketLatticeData.ordinaryDensity line 26
def OAI.LipschitzHilbert.PacketLatticeData.ownBox line 31
Source documentation
The actual spatial rectangle and direction of a source packet.
```
def ownBox (oldSlope : ℝ) (q : P.PacketIndex) : SlopeBox where
…
```
Mentions: OAI.LipschitzHilbert.SlopeBox

def OAI.LipschitzHilbert.PacketLatticeData.ownDensityTest line 41

Source documentation

The ordinary density includes each packet's own rectangle.

def ownDensityTest (oldSlope : ℝ) (cell : ∀ j, P.labels j → ℤ)
    (grid : ℤ) (w tau : ℝ) (q : P.PacketIndex)
    (hlen : P.length q.1≤tau)
    (hslope : oldSlope+P.rowSlope q.1 q.2.1 ∈
      scaledAngularCell (w/P.topLength) grid q.1.val (cell q.1 q.2.1)) :
    OrdinaryDensityTest P.topLength w P.width tau grid (P.densityTile oldSlope cell q) where
…

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

theorem OAI.LipschitzHilbert.PacketLatticeData.own_packet_whitney_density_bound line 64

Source documentation

A literal source packet restricted to a Whitney strip. Its decay factor is precisely the one summed in SourceShortTreeSum.

theorem own_packet_whitney_density_bound
    (oldSlope : ℝ) (cell : ∀ j, P.labels j → ℤ) (grid : ℤ) (w tau : ℝ)
    (q : P.PacketIndex) (hlen : P.length q.1≤tau)
    (hslope : oldSlope+P.rowSlope q.1 q.2.1 ∈
      scaledAngularCell (w/P.topLength) grid q.1.val (cell q.1 q.2.1))
    (horder : 205≤2*P.order) (M sigma eta : ℝ) (hM : 0≤M) (hsigma : 0≤sigma)
    (coefficient : EuclideanSpace ℂ κ) (hcoefficient : ‖coefficient‖≤sigma)
    (selector : κ → ℝ → ℂ) (hselector : ∀ a, Measurable (selector a))
    (hbound : ∀ a s, ‖selector a s‖≤M)
    (hsupport : ∀ a s, selector a s≠0 →
      s∈scaledAngularCell (w/P.topLength) grid q.1.val (cell q.1 q.2.1))
    (u : ℝ×ℝ → ℝ) (hu : Measurable u) (E : Set (ℝ×ℝ)) (hE : MeasurableSet E)
…

Mentions: OAI.LipschitzHilbert.scaledAngularCell