OAI/NumberTheory/DirichletL/MeanSquare/InputEnergy.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.InitialMeanSquare.poolProduct_admissible line 78
  2. theorem OAI.InitialMeanSquare.poolPrimary_norm line 97
  3. theorem OAI.InitialMeanSquare.selectedIdealTest_full_range line 106
  4. theorem OAI.InitialMeanSquare.idealRowSum_initial_energy line 121
  5. theorem OAI.SecondPassArithmetic.inputConjugateRow_zero_of_mass_zero line 162
  6. theorem OAI.SecondPassArithmetic.globalFirstCoreRow_zero_off_support line 178
  7. theorem OAI.SecondPassArithmetic.globalFirstFiniteEnergy_eq_supported line 203
  8. def OAI.SecondPassArithmetic.globalFirstTailFactor line 228
  9. theorem OAI.SecondPassArithmetic.globalFirstPooledRow_lower_from_common line 235
  10. theorem OAI.SecondPassArithmetic.globalFirstTailFactor_bound line 261
  11. theorem OAI.SecondPassArithmetic.globalFirstWeightedVolume_bound line 303
  12. theorem OAI.SecondPassArithmetic.globalFirstTailCost_parent_bound line 361
  13. theorem OAI.SecondPassArithmetic.globalFirstCoreRows_quantitative_transfer line 409
  14. def OAI.SecondPassArithmetic.globalFirstRayChildBudget line 511
  15. def OAI.SecondPassArithmetic.globalFirstQuantitativeBudget line 523
  16. lemma OAI.SecondPassArithmetic.two_finite_error_sum line 532
  17. theorem OAI.SecondPassArithmetic.globalCubeInputFamilyEnergy_quantitative line 542