OAI/Analysis/LipschitzHilbert/Packets/SourcePacketShortSum.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.LipschitzHilbert.SourceLabeledLattice.whitneyAllowed line 17
2. def OAI.LipschitzHilbert.SourceLabeledLattice.shortKernel line 21
3. theorem OAI.LipschitzHilbert.SourceLabeledLattice.label_short_kernel_sum line 24
4. theorem OAI.LipschitzHilbert.SourceLabeledLattice.label_short_kernel_decay_sum line 43
5. theorem OAI.LipschitzHilbert.SourceLabeledLattice.row_short_kernel_sum line 63
6. theorem OAI.LipschitzHilbert.SourceLabeledLattice.packet_short_mass_sum line 78

   Source documentation

   The short-tail majorant summed over every packet with length at most R. Labels cost only their fixed per-scale multiplicity.

   theorem packet_short_mass_sum (B : ℕ) (hcard : ∀ j, (P.labels j).card≤B)
       (y R : ℝ) (hR : 0≤R) (k m : ℤ) (hallowed : P.whitneyAllowed k m)
       (hcenter : ∀ j l u, |P.actualZ j l u-y|≤P.width) :
       (∑ q : P.PacketIndex, if P.length q.1≤R then
         P.length q.1*P.width*P.shortKernel k m q else 0) ≤
         288*(4*Real.pi)^2*B*P.width*R := by
   …

7. theorem OAI.LipschitzHilbert.SourceLabeledLattice.packet_short_mass_decay_sum line 111

   Source documentation

   The far-strip majorant over the entire packet family retains decay in the ratio of top length to Whitney length.

   theorem packet_short_mass_decay_sum (B : ℕ) (hcard : ∀ j, (P.labels j).card≤B)
       (y : ℝ) (k m : ℤ) (hallowed : P.whitneyAllowed k m)
       (hcenter : ∀ j l u, |P.actualZ j l u-y|≤P.width) (hlarge : P.topLength≤DyadicLineGrid.scale k) :
       (∑ q : P.PacketIndex, P.length q.1*P.width*P.shortKernel k m q) ≤
         288*(4*Real.pi)^2*B*P.width*P.topLength*(P.topLength/DyadicLineGrid.scale k)^2 := by
   …

   Mentions: OAI.LipschitzHilbert.DyadicLineGrid.scale