OAI/Analysis/LipschitzHilbert/Trees/SourceReferenceMask.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Actual top masks restricted to the affine reference line. The bandwidth and derivative costs retain the exact top length and slope.

  1. def OAI.LipschitzHilbert.SlopeBox.maskLineA line 15
  2. def OAI.LipschitzHilbert.SlopeBox.maskLineB line 16
  3. def OAI.LipschitzHilbert.SlopeBox.maskLineC line 17
  4. def OAI.LipschitzHilbert.SlopeBox.maskLineD line 18
  5. theorem OAI.LipschitzHilbert.SlopeBox.mask_on_reference_line line 20
  6. theorem OAI.LipschitzHilbert.SlopeBox.mask_on_scaled_reference_line line 27
  7. def OAI.LipschitzHilbert.SlopeBox.maskLineBandwidth line 34
  8. theorem OAI.LipschitzHilbert.SlopeBox.maskLineBandwidth_eq line 37
  9. theorem OAI.LipschitzHilbert.SlopeBox.maskLineBandwidth_packet_le line 49

    Source documentation

    Retained short packets and the actual angular cone give the mask bandwidth at the packet scale.

    theorem maskLineBandwidth_packet_le (T : SlopeBox) (L A t ell R : ℝ)
    (hL : 0 < L) (hell : 0 < ell) (hshort : ell ≤ T.length)
    (hcone : |t-T.slope| ≤ R*T.width/ell) :
    T.maskLineBandwidth L A t ≤
      ((2*(⌈L⌉₊:ℝ))/(2*Real.pi*L^A))*((1+R)/ell) := by
…

    Mentions: OAI.LipschitzHilbert.SlopeBox

  10. def OAI.LipschitzHilbert.SlopeBox.referenceMaskedPacket line 66

    Source documentation

    The actual top mask multiplies the original reference-line packet.

    def referenceMaskedPacket (T : SlopeBox) (L A t y : ℝ)
    (f : SchwartzMap ℝ ℂ) : SchwartzMap ℝ ℂ :=
…

    Mentions: OAI.LipschitzHilbert.SlopeBox

  11. theorem OAI.LipschitzHilbert.SlopeBox.referenceMaskedPacket_apply line 71
  12. theorem OAI.LipschitzHilbert.SlopeBox.referenceMaskedPacket_norm_le line 76
  13. theorem OAI.LipschitzHilbert.SlopeBox.referenceMaskedPacket_deriv_le line 81
  14. theorem OAI.LipschitzHilbert.SlopeBox.referenceMaskedPacket_fourier line 92