OAI/NumberTheory/DirichletL/CubicSieve/IntegratedTransfer.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SecondPassArithmetic.sideRayMonoid_norm_le_one line 88
  2. lemma OAI.SecondPassArithmetic.firstCoreTwist_norm_le line 94
  3. theorem OAI.SecondPassArithmetic.firstCoreOuter_norm_le line 111
  4. theorem OAI.SecondPassArithmetic.firstCoreOuter_mass line 135
  5. theorem OAI.SecondPassArithmetic.dilatedCoreRow_sq_le_input_family line 151
  6. theorem OAI.SecondPassArithmetic.firstCoreTest_continuous line 174
  7. theorem OAI.SecondPassArithmetic.firstCoreTest_norm line 181
  8. def OAI.SecondPassArithmetic.firstCoreInputRow line 188
  9. theorem OAI.SecondPassArithmetic.firstCoreInputRow_continuous line 196
  10. theorem OAI.SecondPassArithmetic.firstCoreInputRow_uniform_bound line 208
  11. theorem OAI.SecondPassArithmetic.firstCoreInputRow_integrable line 229
  12. theorem OAI.SecondPassArithmetic.dilatedCoreRow_energy_le_input_family line 255
  13. theorem OAI.SecondPassArithmetic.normalizedColumn_multiplicativeCoreColumn line 312
  14. def OAI.SecondPassArithmetic.firstInputFamilyEnergy line 320
  15. theorem OAI.SecondPassArithmetic.firstInputFamilyEnergy_nonneg line 331
  16. theorem OAI.SecondPassArithmetic.firstOutputEnergy_le_input_family line 350
  17. theorem OAI.SecondPassArithmetic.firstCoreInputRow_smoothed_sign line 385
  18. theorem OAI.SecondPassArithmetic.firstCoreInputRow_smoothed_second_poisson line 404
  19. abbrev OAI.JointLogSeparation.Frequency line 432
  20. def OAI.JointLogSeparation.tripleCoefficient line 434
  21. lemma OAI.JointLogSeparation.tripleCoefficient_integrable line 437
  22. lemma OAI.JointLogSeparation.tripleCoefficient_bounded_integrable line 441
  23. lemma OAI.JointLogSeparation.tripleCoefficient_norm_bounded_integrable line 447
  24. lemma OAI.JointLogSeparation.tripleCoefficient_slice_integrable line 453
  25. lemma OAI.JointLogSeparation.tripleCoefficient_norm_slice_integrable line 462
  26. lemma OAI.JointLogSeparation.nested_eq_integral line 471
  27. theorem OAI.JointLogSeparation.triple_integral_bound line 480
  28. abbrev OAI.SecondPassIntegration.O line 510
  29. lemma OAI.SecondPassIntegration.fixedTest_continuous line 521
  30. lemma OAI.SecondPassIntegration.fixedColumn_norm_frequency line 528
  31. lemma OAI.SecondPassIntegration.fixedRow_continuous line 535
  32. def OAI.SecondPassIntegration.rowMagnitude line 546
  33. lemma OAI.SecondPassIntegration.rowMagnitude_nonneg line 551
  34. lemma OAI.SecondPassIntegration.fixedRow_norm_le line 556
  35. def OAI.SecondPassIntegration.childEnergy line 564
  36. def OAI.SecondPassIntegration.energyMagnitude line 569
  37. lemma OAI.SecondPassIntegration.childEnergy_nonneg line 575
  38. lemma OAI.SecondPassIntegration.childEnergy_le line 581
  39. lemma OAI.SecondPassIntegration.childEnergy_continuous line 592
  40. def OAI.SecondPassIntegration.integratedSecondMode line 618
  41. def OAI.SecondPassIntegration.childGeometricMean line 625
  42. theorem OAI.SecondPassIntegration.integrated_fixed_second_mode_transfer line 630