OAI/NumberTheory/DirichletL/Inversion/InitialPhysicalMeasure.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.SevenEighths.InverseInitialPhysicalMeasure.Point line 17
  2. def OAI.SevenEighths.InverseInitialPhysicalMeasure.divisor line 30
  3. def OAI.SevenEighths.InverseInitialPhysicalMeasure.quotient line 32
  4. def OAI.SevenEighths.InverseInitialPhysicalMeasure.coordinates line 34
  5. structure OAI.SevenEighths.InverseInitialPhysicalMeasure.Valid line 38
  6. theorem OAI.SevenEighths.InverseInitialPhysicalMeasure.coordinates_pos line 46
  7. theorem OAI.SevenEighths.InverseInitialPhysicalMeasure.divisor_span line 51
  8. theorem OAI.SevenEighths.InverseInitialPhysicalMeasure.quotient_span line 57
  9. theorem OAI.SevenEighths.InverseInitialPhysicalMeasure.common_span line 64
  10. def OAI.SevenEighths.InverseInitialPhysicalMeasure.unitSector line 71
  11. theorem OAI.SevenEighths.InverseInitialPhysicalMeasure.unitSector_spec line 77
  12. theorem OAI.SevenEighths.InverseInitialPhysicalMeasure.child_normalized line 82
  13. theorem OAI.SevenEighths.InverseInitialPhysicalMeasure.column_extraction line 99
  14. def OAI.SevenEighths.InverseInitialPhysicalMeasure.outerCoefficient line 120
  15. def OAI.SevenEighths.InverseInitialPhysicalMeasure.canonicalColumn line 128
  16. def OAI.SevenEighths.InverseInitialPhysicalMeasure.physicalTerm line 136
  17. theorem OAI.SevenEighths.InverseInitialPhysicalMeasure.physicalTerm_extracted line 150
  18. def OAI.SevenEighths.InverseInitialPhysicalMeasure.barePair line 167
  19. def OAI.SevenEighths.InverseInitialPhysicalMeasure.columnRatio line 173
  20. theorem OAI.SevenEighths.InverseInitialPhysicalMeasure.relative_column_left line 177
  21. theorem OAI.SevenEighths.InverseInitialPhysicalMeasure.relative_column_right line 181
  22. theorem OAI.SevenEighths.InverseInitialPhysicalMeasure.columnRatio_actual line 185
  23. def OAI.SevenEighths.InverseInitialPhysicalMeasure.canonicalPairMode line 190
  24. theorem OAI.SevenEighths.InverseInitialPhysicalMeasure.canonical_pair_mode line 201
  25. theorem OAI.SevenEighths.InverseInitialPhysicalMeasure.family_density_finite_sum line 215
  26. def OAI.SevenEighths.InverseInitialPhysicalMeasure.physicalBlock line 233
  27. def OAI.SevenEighths.InverseInitialPhysicalMeasure.canonicalBlock line 238
  28. theorem OAI.SevenEighths.InverseInitialPhysicalMeasure.physicalBlock_integral line 243
  29. theorem OAI.SevenEighths.InverseInitialPhysicalMeasure.original_ray_common_insertion line 304
  30. theorem OAI.SevenEighths.InverseInitialPhysicalMeasure.physicalBlock_zero line 328
  31. theorem OAI.SevenEighths.InverseInitialPhysicalMeasure.child_test_clipping line 339
  32. def OAI.SevenEighths.InverseInitialPhysicalMeasure.BlockSupport line 350
  33. theorem OAI.SevenEighths.InverseInitialPhysicalMeasure.actual_initial_block_common_measure line 361
  34. def OAI.SevenEighths.InverseInitialPhysicalMeasure.overlapDilation line 408
  35. theorem OAI.SevenEighths.InverseInitialPhysicalMeasure.residualWindow_eq_clipped line 411
  36. theorem OAI.SevenEighths.InverseInitialPhysicalMeasure.overlapDilation_pos line 418
  37. theorem OAI.SevenEighths.InverseInitialPhysicalMeasure.clippedSource_zero_star line 425
  38. def OAI.SevenEighths.InverseInitialPhysicalMeasure.originalBlock line 430
  39. theorem OAI.SevenEighths.InverseInitialPhysicalMeasure.originalBlock_integral line 444