OAI/NumberTheory/DirichletL/Inversion/TerminalWidths.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SevenEighths.InverseTerminalWidths.norm_one_le line 13
  2. theorem OAI.SevenEighths.InverseTerminalWidths.physical_residual_width line 16
  3. theorem OAI.SevenEighths.InverseTerminalWidths.constant_log_error line 43
  4. def OAI.SevenEighths.InverseTerminalWidths.activeCharge line 55
  5. theorem OAI.SevenEighths.InverseTerminalWidths.activeCharge_le_two line 58
  6. theorem OAI.SevenEighths.InverseTerminalWidths.activeCharge_le_one line 62
  7. theorem OAI.SevenEighths.InverseTerminalWidths.reflectionLocalCost_eq_charge line 69
  8. theorem OAI.SevenEighths.InverseTerminalWidths.surviving_local_piece line 74
  9. def OAI.SevenEighths.InverseTerminalWidths.normWidth line 90
  10. def OAI.SevenEighths.InverseTerminalWidths.reflectionWidth line 92
  11. theorem OAI.SevenEighths.InverseTerminalWidths.reflectionConductorCost_pos line 98
  12. theorem OAI.SevenEighths.InverseTerminalWidths.logb_reflectionConductorCost line 110
  13. theorem OAI.SevenEighths.InverseTerminalWidths.reflection_charge_width line 126
  14. theorem OAI.SevenEighths.InverseTerminalWidths.normWidth_upper line 157
  15. theorem OAI.SevenEighths.InverseTerminalWidths.normWidth_lower line 166
  16. def OAI.SevenEighths.InverseTerminalWidths.terminalDualWidth line 173
  17. def OAI.SevenEighths.InverseTerminalWidths.widthConstant line 179
  18. theorem OAI.SevenEighths.InverseTerminalWidths.logb_widthConstant line 182
  19. theorem OAI.SevenEighths.InverseTerminalWidths.terminal_common_width line 194
  20. theorem OAI.SevenEighths.InverseTerminalWidths.normWidth_nonneg line 222
  21. theorem OAI.SevenEighths.InverseTerminalWidths.rpow_reflectionWidth line 225
  22. theorem OAI.SevenEighths.InverseTerminalWidths.width_error_threshold line 232
  23. theorem OAI.SevenEighths.InverseTerminalWidths.canonical_active_pool line 245
  24. theorem OAI.SevenEighths.InverseTerminalWidths.surviving_inactive_exponent line 257
  25. theorem OAI.SevenEighths.InverseTerminalWidths.surviving_reflected_branch line 274
  26. theorem OAI.SevenEighths.InverseTerminalWidths.canonical_terminal_common_width line 286
  27. def OAI.SevenEighths.InverseTerminalWidths.hybridSaving line 318
  28. def OAI.SevenEighths.InverseTerminalWidths.reflectedExponent line 320
  29. theorem OAI.SevenEighths.InverseTerminalWidths.hybridSaving_nonneg line 324
  30. theorem OAI.SevenEighths.InverseTerminalWidths.hybridSaving_half line 327
  31. theorem OAI.SevenEighths.InverseTerminalWidths.terminal_width_from_invariant line 339
  32. theorem OAI.SevenEighths.InverseTerminalWidths.reflected_row_bound line 348
  33. theorem OAI.SevenEighths.InverseTerminalWidths.reflected_column_full_bound line 359
  34. theorem OAI.SevenEighths.InverseTerminalWidths.reflected_column_partial_bound line 369
  35. theorem OAI.SevenEighths.InverseTerminalWidths.reflected_terminal_cases line 381
  36. theorem OAI.SevenEighths.InverseTerminalWidths.reflected_terminal_saving line 407
  37. def OAI.SevenEighths.InverseTerminalWidths.ramifiedWidth line 428
  38. theorem OAI.SevenEighths.InverseTerminalWidths.rpow_ramifiedWidth line 430
  39. theorem OAI.SevenEighths.InverseTerminalWidths.fractionalThetaPoint_norm_width line 436
  40. theorem OAI.SevenEighths.InverseTerminalWidths.ramified_width_threshold line 444
  41. theorem OAI.SevenEighths.InverseTerminalWidths.terminal_error_threshold line 459
  42. theorem OAI.SevenEighths.InverseTerminalWidths.actual_terminal_saving line 472
  43. theorem OAI.SevenEighths.InverseTerminalWidths.residual_admissible_of_fixed_bad line 512
  44. def OAI.SevenEighths.InverseTerminalWidths.canonicalDualWidth line 519
  45. def OAI.SevenEighths.InverseTerminalWidths.canonicalExtractedWidth line 527
  46. theorem OAI.SevenEighths.InverseTerminalWidths.canonical_terminal_saving line 534