OAI/Analysis/LipschitzHilbert/Phase/SourceAngularTreeSplit.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LipschitzHilbert.SourceLabeledLattice.longErrorLocalAtWidth line 18
2. theorem OAI.LipschitzHilbert.SourceLabeledLattice.frozenLongValue_eq_selector_at_width line 27
3. theorem OAI.LipschitzHilbert.SourceLabeledLattice.longErrorLocalAtWidth_measurable line 43
4. theorem OAI.LipschitzHilbert.SourceLabeledLattice.longErrorLocalAtWidth_bound line 57

   Source documentation

   The dyadic selector-error estimate applies to the exact long restriction without paying for the number of scales.

   theorem longErrorLocalAtWidth_bound (w : ℝ) (hw : 0<w) (K B : ℕ) (horder : 107≤P.order)
       (hcard : ∀ j, (P.labels j).card≤B) (b radius Cb M Lip sigma : ℝ)
       (hM : 0≤M) (hLip : 0≤Lip) (hsigma : 0≤sigma)
       (hwide : 1≤radius+Cb) (hK : radius+Cb≤(2:ℝ)^K)
       (hcenter : ∀ j l v, |P.actualZ j l v-b|≤P.width)
       (hslope : ∀ j l, |P.rowSlope j l|≤Cb*(w/P.length j))
       (c : ∀ j (l : P.labels j), Item j l → EuclideanSpace ℂ κ)
       (hc : ∀ j l v, ‖c j l v‖≤sigma)
       (selector : ∀ j, P.labels j → κ → ℝ → ℂ)
       (hbound : ∀ j l k s, ‖selector j l k s‖≤M)
       (hsupport : ∀ j l k s, selector j l k s≠0 →
         |s-P.rowSlope j l|≤radius*(w/P.length j))
   …

5. theorem OAI.LipschitzHilbert.SourceLabeledLattice.longOriginalLocal_mask_at_width line 85

   Source documentation

   Only the original selector support is used to insert the common mask.

   theorem longOriginalLocal_mask_at_width (w : ℝ)
       (c : ∀ j (l : P.labels j), Item j l → EuclideanSpace ℂ κ)
       (selector : ∀ j, P.labels j → κ → ℝ → ℂ) (u : ℝ×ℝ → ℝ)
       (cell : ∀ j, P.labels j → ℤ) (grid : ℤ)
       (hsupport : ∀ j l k s, selector j l k s≠0 →
         s∈scaledAngularCell (w/P.topLength) grid j.val (cell j l))
       (Omega : P.DensityWhitneyCell → Set ℝ)
       (hcontains : ∀ i (q : P.PacketIndex), 32*DyadicLineGrid.scale i.val.1<P.length q.1 →
         scaledAngularCell (w/P.topLength) grid q.1.val (cell q.1 q.2.1)⊆Omega i)
       (E : Set (ℝ×ℝ)) (i : P.DensityWhitneyCell) (z : ℝ×ℝ) :
       E.indicator (P.longOriginalLocal c selector u i) z=
         (E∩u ⁻¹' Omega i).indicator (P.longOriginalLocal c selector u i) z := by
   …

   Mentions: OAI.LipschitzHilbert.scaledAngularCell, OAI.LipschitzHilbert.DyadicLineGrid.scale

6. def OAI.LipschitzHilbert.SourceLabeledLattice.longErrorTreeValueAtWidth line 115
7. theorem OAI.LipschitzHilbert.SourceLabeledLattice.angular_long_error_integrable_bound line 126
8. theorem OAI.LipschitzHilbert.SourceLabeledLattice.angular_ordinary_tree_split_identity line 164