OAI/NumberTheory/JointDickman/Amplification/AmplificationBoxSupport.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Exact support of the amplification integrand in each geometric box

  1. theorem OAI.JointDickman.mem_tensor_interval_of_ratio line 11
  2. theorem OAI.JointDickman.amplificationBoxWeight_integer_support line 23
  3. def OAI.JointDickman.amplificationArithmeticTerm line 33
  4. def OAI.JointDickman.amplificationBoxTerm line 42
  5. theorem OAI.JointDickman.amplificationBoxTerm_support line 51
  6. theorem OAI.JointDickman.amplificationBoxTerm_eq line 64
  7. theorem OAI.JointDickman.amplificationArithmeticTerm_log_support line 76