OAI/Analysis/LipschitzHilbert/Trees/SourceShortTreeIntegral.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LipschitzHilbert.SourceLabeledLattice.ordinaryPacketValue line 17

   Source documentation

   Original packet with its coefficient and original selector.

   def ordinaryPacketValue (P : SourceLabeledLattice N κ Label Item) (oldSlope : ℝ)
       (coefficient : P.PacketIndex → EuclideanSpace ℂ κ)
       (selector : ∀ j, P.labels j → κ → ℝ → ℂ) (u : ℝ×ℝ → ℝ)
       (q : P.PacketIndex) (z : ℝ×ℝ) : EuclideanSpace ℂ κ :=
   …

   Mentions: OAI.LipschitzHilbert.SourceLabeledLattice

2. theorem OAI.LipschitzHilbert.SourceLabeledLattice.short_tree_finite_strip_bound line 28

   Source documentation

   Sum of absolute short-packet integrals over any finite family of actual Whitney strips is bounded by size times density times top area. The explicit constant depends only on the fixed packet seminorm, label multiplicity, selector bound, and short/long splitting constant.

   theorem short_tree_finite_strip_bound (P : SourceLabeledLattice N κ Label Item)
       (B : ℕ) (hcard : ∀ j, (P.labels j).card≤B)
       (oldSlope : ℝ) (cell : ∀ j, P.labels j → ℤ) (grid : ℤ) (w tau : ℝ)
       (htime : P.topLength≤tau)
       (hslope : ∀ j l, oldSlope+P.rowSlope j l ∈
         scaledAngularCell (w/P.topLength) grid j.val (cell j l))
       (horder : 205≤2*P.order) (M sigma eta : ℝ)
       (hM : 0≤M) (hsigma : 0≤sigma) (heta : 0≤eta)
       (coefficient : P.PacketIndex → EuclideanSpace ℂ κ)
       (hcoefficient : ∀ q, ‖coefficient q‖≤sigma)
       (selector : ∀ j, P.labels j → κ → ℝ → ℂ)
       (hselector : ∀ j l a, Measurable (selector j l a))
   …

   Mentions: OAI.LipschitzHilbert.SourceLabeledLattice, OAI.LipschitzHilbert.scaledAngularCell