OAI/NumberTheory/JointDickman/Amplification/EndpointFourierReflection.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Reflecting the second endpoint in the Fourier integral

  1. theorem OAI.JointDickman.finiteAdditiveSum_neg_real line 11
  2. theorem OAI.JointDickman.endpointFourierSum_neg_norm line 22
  3. theorem OAI.JointDickman.endpointFourierSum_continuous line 29