OAI/Analysis/LipschitzHilbert/Fourier/ModulatedInverseL1.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Joint parameter continuity of the inverse modulated multiplier only needs integrable frequency data, so it applies to amplitude slices.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.modulated_inverse_joint_continuous_l1 line 11