OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/E.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.OrdinaryChainScales.E line 21
  2. def OAI.OrdinaryChainScales.F line 22
  3. def OAI.OrdinaryChainScales.mesh line 23
  4. def OAI.OrdinaryChainScales.amplifier line 24
  5. lemma OAI.OrdinaryChainScales.E_pos line 26
  6. lemma OAI.OrdinaryChainScales.F_pos line 27
  7. lemma OAI.OrdinaryChainScales.mesh_pos line 28
  8. lemma OAI.OrdinaryChainScales.E_le_F line 29
  9. lemma OAI.OrdinaryChainScales.F_eq line 33
  10. lemma OAI.OrdinaryChainScales.next_E line 39
  11. lemma OAI.OrdinaryChainScales.next_F line 45
  12. lemma OAI.OrdinaryChainScales.mesh_E line 51
  13. lemma OAI.OrdinaryChainScales.next_mesh_F line 59
  14. lemma OAI.OrdinaryChainScales.mesh_mono line 67
  15. lemma OAI.OrdinaryChainScales.E_mono line 73
  16. lemma OAI.OrdinaryChainScales.F_mono line 79
  17. lemma OAI.OrdinaryChainScales.amplifier_lower line 85
  18. lemma OAI.OrdinaryChainScales.amplifier_upper line 88
  19. lemma OAI.OrdinaryChainScales.amplifier_bound line 93
  20. lemma OAI.OrdinaryChainScales.amplifier_square_absorption line 110
  21. lemma OAI.OrdinaryChainScales.previous_scale_absorption line 129
  22. lemma OAI.OrdinaryChainScales.next_gain line 134