OAI/Analysis/LipschitzHilbert/Trees/SourceTreeSelectorError.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

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

   Source documentation

   Arbitrary coordinate multipliers on the actual raw packets.

   def rawSelectorTreeValue (i : Fin 3)
       (c : ∀ j (l : P.labels j), Item j l → EuclideanSpace ℂ κ)
       (beta : ∀ j, P.labels j → κ → ℂ) (y x : ℝ) : EuclideanSpace ℂ κ :=
   …

2. theorem OAI.LipschitzHilbert.SourceLabeledLattice.rawSelectorTreeValue_sub line 23
3. theorem OAI.LipschitzHilbert.SourceLabeledLattice.tree_raw_envelope line 32
4. theorem OAI.LipschitzHilbert.SourceLabeledLattice.tree_transverse_overlap line 49
5. theorem OAI.LipschitzHilbert.SourceLabeledLattice.raw_tree_selector_error line 99

   Source documentation

   The source-angle error at a fixed point has summable dyadic size. The multiplier hypotheses concern the original selectors, not the error.

   theorem raw_tree_selector_error (q K B : ℕ) (horder : 1+2*q≤P.order)
       (hcard : ∀ j, (P.labels j).card≤B) (w b t radius Cb M Lip sigma : ℝ)
       (hw : 0<w) (hM : 0≤M) (hLip : 0≤Lip) (hsigma : 0≤sigma)
       (hwide : 1≤radius+Cb) (hK : radius+Cb≤(2:ℝ)^K)
       (hcenter : ∀ j l u, |P.actualZ j l u-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 u, ‖c j l u‖≤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-(t+P.rowSlope j l)|≤radius*(w/P.length j))
   …

6. def OAI.LipschitzHilbert.SourceLabeledLattice.physicalTreeSelectorValue line 219

   Source documentation

   The original physical packet sum, before restriction to its common angular-support set.

   def physicalTreeSelectorValue (t : ℝ)
       (c : ∀ j (l : P.labels j), Item j l → EuclideanSpace ℂ κ)
       (beta : ∀ j, P.labels j → κ → ℂ) (z : ℝ×ℝ) : EuclideanSpace ℂ κ :=
   …

7. theorem OAI.LipschitzHilbert.SourceLabeledLattice.physicalTreeSelectorValue_eq_raw line 225
8. theorem OAI.LipschitzHilbert.SourceLabeledLattice.physical_tree_freezing_error line 240

   Source documentation

   Both the original sum and its frozen replacement keep the same angular indicator. No support assertion about the frozen sum is used.

   theorem physical_tree_freezing_error (q K B : ℕ) (horder : 1+2*q≤P.order)
       (hcard : ∀ j, (P.labels j).card≤B) (w b t radius Cb M Lip sigma : ℝ)
       (hw : 0<w) (hM : 0≤M) (hLip : 0≤Lip) (hsigma : 0≤sigma)
       (hwide : 1≤radius+Cb) (hK : radius+Cb≤(2:ℝ)^K)
       (hcenter : ∀ j l u, |P.actualZ j l u-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 u, ‖c j l u‖≤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-(t+P.rowSlope j l)|≤radius*(w/P.length j))
   …