OAI/NumberTheory/DirichletL/Inversion/InitialConjugateEnergy.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.InverseInitialConjugateEnergy.conjugateIdealCharacter line 15
  2. theorem OAI.SevenEighths.InverseInitialConjugateEnergy.conjugateIdealCharacter_apply line 20
  3. theorem OAI.SevenEighths.InverseInitialConjugateEnergy.reconstructedSelector_conjugate line 23
  4. theorem OAI.SevenEighths.InverseInitialConjugateEnergy.overlapResidualCoefficient_conjugate line 30
  5. def OAI.SevenEighths.InverseInitialConjugateEnergy.conjugatedResidual line 37
  6. theorem OAI.SevenEighths.InverseInitialConjugateEnergy.star_conjugatedResidual line 42
  7. theorem OAI.SevenEighths.InverseInitialConjugateEnergy.originalFixedPolynomial_eq_conjugatedResidual line 52
  8. theorem OAI.SevenEighths.InverseInitialConjugateEnergy.originalFixedPolynomial_norm_sq_conjugatedResidual line 64
  9. theorem OAI.SevenEighths.InverseInitialConjugateEnergy.admissible_row_four_le_one line 83
  10. theorem OAI.SevenEighths.InverseInitialConjugateEnergy.originalFixedPolynomial_norm_sq_le line 91
  11. theorem OAI.SevenEighths.InverseInitialConjugateEnergy.finite_weighted_triangle line 103
  12. theorem OAI.SevenEighths.InverseInitialConjugateEnergy.weighted_overlap_triangle line 126
  13. def OAI.SevenEighths.InverseInitialConjugateEnergy.radialWeight line 143
  14. def OAI.SevenEighths.InverseInitialConjugateEnergy.smoothedEnergy line 146
  15. theorem OAI.SevenEighths.InverseInitialConjugateEnergy.radialWeight_nonneg line 149
  16. theorem OAI.SevenEighths.InverseInitialConjugateEnergy.smoothedEnergy_nonneg line 153
  17. theorem OAI.SevenEighths.InverseInitialConjugateEnergy.original_energy_summable line 157
  18. theorem OAI.SevenEighths.InverseInitialConjugateEnergy.conjugatedResidual_energy_summable line 166
  19. theorem OAI.SevenEighths.InverseInitialConjugateEnergy.original_smoothed_mask_identity line 176
  20. theorem OAI.SevenEighths.InverseInitialConjugateEnergy.original_smoothed_contraction line 190
  21. theorem OAI.SevenEighths.InverseInitialConjugateEnergy.sqrt_overlap_prefactor line 208
  22. def OAI.SevenEighths.InverseInitialConjugateEnergy.originalTotalPolynomial line 219
  23. theorem OAI.SevenEighths.InverseInitialConjugateEnergy.originalTotalPolynomial_eq_sectors line 224
  24. theorem OAI.SevenEighths.InverseInitialConjugateEnergy.original_smoothed_overlap_triangle line 236
  25. theorem OAI.SevenEighths.InverseInitialConjugateEnergy.real_smoothed_sum_eq line 258
  26. theorem OAI.SevenEighths.InverseInitialConjugateEnergy.original_smoothed_overlap_bound line 272
  27. def OAI.SevenEighths.InverseInitialConjugateEnergy.conjugatePhysicalSum line 284
  28. theorem OAI.SevenEighths.InverseInitialConjugateEnergy.conjugatedResidual_physical line 301
  29. theorem OAI.SevenEighths.InverseInitialConjugateEnergy.conjugatedResidual_energy_physical line 311
  30. theorem OAI.SevenEighths.InverseInitialConjugateEnergy.original_fixed_physical_contraction line 326
  31. theorem OAI.SevenEighths.InverseInitialConjugateEnergy.original_physical_overlap_triangle line 337
  32. theorem OAI.SevenEighths.InverseInitialConjugateEnergy.original_smoothed_overlap_cauchy line 355
  33. theorem OAI.SevenEighths.InverseInitialConjugateEnergy.original_complex_physical_overlap_bound line 375