SourceTreeErrorIntegral.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Integrating the ordinary-tree error over the actual density masks. Order 53 leaves at least six decay powers after the density loss 203.

theorem OAI.LipschitzHilbert.error_cell_integral line 15

theorem OAI.LipschitzHilbert.SourceLabeledLattice.tree_error_integrable_bound line 63

Source documentation

A pointwise transverse error estimate integrates with the actual cell masks at a cost independent of the number of scales and cells.

theorem tree_error_integrable_bound (hne : Nonempty P.PacketIndex)
    (F : P.DensityWhitneyCell → ℝ×ℝ → EuclideanSpace ℂ κ)
    (hF : ∀ i, AEStronglyMeasurable (F i) (volume.prod volume))
    (a b D eta : ℝ) (hD : 0≤D) (heta : 0≤eta)
    (hcenter : ∀ q : P.PacketIndex, |P.actualX q.1 q.2.1 q.2.2-a|≤P.topLength/2)
    (hbound : ∀ i z, polynomialWeight b (2*P.width) 53 z.2^2*‖F i z‖≤D)
    (E : Set (ℝ×ℝ)) (hE : MeasurableSet E) (u : ℝ×ℝ → ℝ) (hu : Measurable u)
    (Omega : P.DensityWhitneyCell → Set ℝ) (hOmega : ∀ i, MeasurableSet (Omega i))
    (hEmpty : ∀ i, ¬P.HasLongPacket i → Omega i=∅)
    (hmass : ∀ i n, (volume.prod volume).real
      (partitionCell b P.width (i.val,n)∩(E∩u ⁻¹' Omega i))≤
      32*(2:ℝ)^203*eta*(1+|(n:ℝ)|)^203*DyadicLineGrid.scale i.val.1*P.width) :
…

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