SourceLongTreeSplit.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

The original long sum, its frozen coefficients, and the literal selector error. No support property is imposed on the frozen sum.

def OAI.LipschitzHilbert.SourceLabeledLattice.longCoefficient line 18
def OAI.LipschitzHilbert.SourceLabeledLattice.frozenSelectorCoefficient line 23
def OAI.LipschitzHilbert.SourceLabeledLattice.longOriginalLocal line 29
def OAI.LipschitzHilbert.SourceLabeledLattice.longErrorLocal line 36
theorem OAI.LipschitzHilbert.SourceLabeledLattice.longCoefficient_norm_le line 44
theorem OAI.LipschitzHilbert.SourceLabeledLattice.frozenLongValue_eq_selector line 53
theorem OAI.LipschitzHilbert.SourceLabeledLattice.physicalTreeSelectorValue_measurable line 68
theorem OAI.LipschitzHilbert.SourceLabeledLattice.longErrorLocal_measurable line 86

theorem OAI.LipschitzHilbert.SourceLabeledLattice.longErrorLocal_bound line 100

Source documentation

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

theorem longErrorLocal_bound (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*(P.width/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*(P.width/P.length j))
…

theorem OAI.LipschitzHilbert.SourceLabeledLattice.frozenSelectorCoefficient_norm_le line 128

Source documentation

Coordinate multipliers of norm at most one do not enlarge the coefficient size used by the frozen tree estimate.

theorem frozenSelectorCoefficient_norm_le
    (c : ∀ j (l : P.labels j), Item j l → EuclideanSpace ℂ κ)
    (selector : ∀ j, P.labels j → κ → ℝ → ℂ)
    (hb : ∀ j l k, ‖selector j l k 0‖≤1)
    (j : Fin N) (l : P.labels j) (v : Item j l) :
    ‖P.frozenSelectorCoefficient c selector j l v‖≤‖c j l v‖ := by
…

theorem OAI.LipschitzHilbert.SourceLabeledLattice.physicalTreeSelectorValue_eq_sum line 137
theorem OAI.LipschitzHilbert.SourceLabeledLattice.longOriginalLocal_eq_sum line 145
theorem OAI.LipschitzHilbert.SourceLabeledLattice.ordinaryTreeLocal_split line 161

theorem OAI.LipschitzHilbert.SourceLabeledLattice.longOriginalLocal_mask line 177

Source documentation

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

theorem longOriginalLocal_mask
    (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 (P.width/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 (P.width/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