OAI/Analysis/LipschitzHilbert/Packets/AnnularPacketGeometry.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Fixed numerical choices for the annular multiplier. The enlargement and compact master radius depend only on its support and on the two frequency-window widths.

  1. structure OAI.LipschitzHilbert.PacketRepresentation.AnnularPacketGeometry line 12
  2. def OAI.LipschitzHilbert.PacketRepresentation.AnnularPacketGeometry.inner line 34
  3. def OAI.LipschitzHilbert.PacketRepresentation.AnnularPacketGeometry.outer line 35
  4. theorem OAI.LipschitzHilbert.PacketRepresentation.AnnularPacketGeometry.H_pos line 36
  5. theorem OAI.LipschitzHilbert.PacketRepresentation.AnnularPacketGeometry.inner_pos line 37
  6. theorem OAI.LipschitzHilbert.PacketRepresentation.AnnularPacketGeometry.outer_pos line 38
  7. def OAI.LipschitzHilbert.PacketRepresentation.AnnularPacketGeometry.numerics line 40
  8. theorem OAI.LipschitzHilbert.PacketRepresentation.AnnularPacketGeometry.parameter_bound line 46
  9. theorem OAI.LipschitzHilbert.PacketRepresentation.exists_annular_packet_geometry line 68

    Source documentation

    The required geometry follows from a narrow horizontal window; all large constants are chosen before the scale, carrier, or row families.

    theorem exists_annular_packet_geometry (A B c C a M : ℝ)
    (hA : 0≤A) (hB : 0≤B) (hc : 0<c) (hC : 0<C) (ha : 0<a) (hM : 0<M)
    (hnarrow : A≤a/4) (hsep : A/c<(3*a/(4*C)/2)/4) :
    Nonempty (AnnularPacketGeometry A B c C a M) := by
…

    Mentions: OAI.LipschitzHilbert.PacketRepresentation.AnnularPacketGeometry