OAI/NumberTheory/DirichletL/Inversion/InitialKernelBridge.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.InverseInitialKernelBridge.pairRow line 21
  2. def OAI.SevenEighths.InverseInitialKernelBridge.pairGauss line 24
  3. def OAI.SevenEighths.InverseInitialKernelBridge.pairCoordinates line 28
  4. theorem OAI.SevenEighths.InverseInitialKernelBridge.common_left_product line 33
  5. theorem OAI.SevenEighths.InverseInitialKernelBridge.common_right_product line 38
  6. theorem OAI.SevenEighths.InverseInitialKernelBridge.conductor_norm line 43
  7. def OAI.SevenEighths.InverseInitialKernelBridge.pairArithmetic line 55
  8. def OAI.SevenEighths.InverseInitialKernelBridge.pairMode line 59
  9. theorem OAI.SevenEighths.InverseInitialKernelBridge.pairKernel_eq_modes line 68
  10. theorem OAI.SevenEighths.InverseInitialKernelBridge.physicalKernel_vector line 74
  11. theorem OAI.SevenEighths.InverseInitialKernelBridge.pairMode_physical line 81
  12. theorem OAI.SevenEighths.InverseInitialKernelBridge.pairKernel_physical line 100
  13. def OAI.SevenEighths.InverseInitialKernelBridge.idealPhysicalPair line 115
  14. theorem OAI.SevenEighths.InverseInitialKernelBridge.ideal_conductor_norm_sq line 125
  15. theorem OAI.SevenEighths.InverseInitialKernelBridge.idealPairKernel_physical line 132
  16. def OAI.SevenEighths.InverseInitialKernelBridge.bareOverlapCoefficient line 145
  17. def OAI.SevenEighths.InverseInitialKernelBridge.maskedOverlapWindow line 149
  18. def OAI.SevenEighths.InverseInitialKernelBridge.residualOverlapWindow line 152
  19. theorem OAI.SevenEighths.InverseInitialKernelBridge.overlapCoefficient_masked line 155
  20. theorem OAI.SevenEighths.InverseInitialKernelBridge.overlapCoefficient_residual line 165
  21. theorem OAI.SevenEighths.InverseInitialKernelBridge.original_fixed_overlap_physical line 171
  22. theorem OAI.SevenEighths.InverseInitialKernelBridge.residual_normalized_physical line 215
  23. def OAI.SevenEighths.InverseInitialKernelBridge.physicalCoordinates line 250
  24. theorem OAI.SevenEighths.InverseInitialKernelBridge.physicalCoordinates_pos line 253
  25. theorem OAI.SevenEighths.InverseInitialKernelBridge.physicalKernel_common_factor line 268
  26. theorem OAI.SevenEighths.InverseInitialKernelBridge.pairCoordinates_eq line 289
  27. theorem OAI.SevenEighths.InverseInitialKernelBridge.pairArithmetic_residual_rows line 294
  28. theorem OAI.SevenEighths.InverseInitialKernelBridge.pairMode_summable line 306
  29. theorem OAI.SevenEighths.InverseInitialKernelBridge.pairMode_zero_split line 318
  30. theorem OAI.SevenEighths.InverseInitialKernelBridge.physicalMode_zero_split line 324
  31. theorem OAI.SevenEighths.InverseInitialKernelBridge.common_extracted_physical_mode line 340
  32. theorem OAI.SevenEighths.InverseInitialKernelBridge.pairDivisor_dvd_common line 371
  33. theorem OAI.SevenEighths.InverseInitialKernelBridge.pairDivisor_span line 376
  34. theorem OAI.SevenEighths.InverseInitialKernelBridge.physicalCoordinates_frequency_ideal line 380