OAI/NumberTheory/Jacobsthal/Analysis/DensityComparison.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.Erdos970Dependency.InitialDensityFormulas.initialTwoDensity line 16
  2. def OAI.Erdos970.Erdos970Dependency.InitialDensityFormulas.regTwoDensity line 19
  3. def OAI.Erdos970.Erdos970Dependency.InitialDensityFormulas.regThreeDensity line 22
  4. def OAI.Erdos970.Erdos970Dependency.InitialDensityFormulas.initialIncoming line 25
  5. def OAI.Erdos970.Erdos970Dependency.InitialDensityFormulas.regTwoIncoming line 28
  6. def OAI.Erdos970.Erdos970Dependency.InitialDensityFormulas.regThreeIncoming line 31
  7. theorem OAI.Erdos970.Erdos970Dependency.InitialDensityFormulas.regTwoDensity_measurable line 34
  8. theorem OAI.Erdos970.Erdos970Dependency.InitialDensityFormulas.regTwoDensity_nonneg line 37
  9. theorem OAI.Erdos970.Erdos970Dependency.InitialDensityFormulas.initialIncoming_formula line 44
  10. theorem OAI.Erdos970.Erdos970Dependency.InitialDensityFormulas.initialIncoming_zero line 68
  11. theorem OAI.Erdos970.Erdos970Dependency.InitialDensityFormulas.regTwoIncoming_formula line 74
  12. theorem OAI.Erdos970.Erdos970Dependency.InitialDensityFormulas.regTwoIncoming_zero line 97
  13. theorem OAI.Erdos970.Erdos970Dependency.InitialDensityFormulas.regThreeIncoming_formula line 107
  14. theorem OAI.Erdos970.Erdos970Dependency.InitialDensityFormulas.regThreeIncoming_zero line 129
  15. theorem OAI.Erdos970.Erdos970Dependency.CompactIncomingIntegrals.initialIncoming_integrable line 146
  16. theorem OAI.Erdos970.Erdos970Dependency.CompactIncomingIntegrals.regTwoIncoming_integrable line 158
  17. theorem OAI.Erdos970.Erdos970Dependency.CompactIncomingIntegrals.regThreeIncoming_integrable line 170
  18. theorem OAI.Erdos970.Erdos970Dependency.CompactIncomingIntegrals.initialIncoming_integral line 180
  19. theorem OAI.Erdos970.Erdos970Dependency.CompactIncomingIntegrals.regTwoIncoming_integral line 191
  20. theorem OAI.Erdos970.Erdos970Dependency.CompactIncomingIntegrals.regThreeIncoming_integral line 201
  21. def OAI.Erdos970.Erdos970Dependency.MarginalDensityMeasures.initialTwoMeasure line 225
  22. def OAI.Erdos970.Erdos970Dependency.MarginalDensityMeasures.regTwoMeasure line 226
  23. def OAI.Erdos970.Erdos970Dependency.MarginalDensityMeasures.regThreeMeasure line 227
  24. instance OAI.Erdos970.Erdos970Dependency.MarginalDensityMeasures.initialTwoMeasure_isProbabilityMeasure line 229
  25. instance OAI.Erdos970.Erdos970Dependency.MarginalDensityMeasures.regTwoMeasure_isProbabilityMeasure line 232
  26. instance OAI.Erdos970.Erdos970Dependency.MarginalDensityMeasures.regThreeMeasure_isProbabilityMeasure line 233
  27. theorem OAI.Erdos970.Erdos970Dependency.MarginalDensityMeasures.even_input_measurable line 235
  28. theorem OAI.Erdos970.Erdos970Dependency.MarginalDensityMeasures.odd_input_measurable line 238
  29. theorem OAI.Erdos970.Erdos970Dependency.MarginalDensityMeasures.evenKernel_eq_density line 241
  30. theorem OAI.Erdos970.Erdos970Dependency.MarginalDensityMeasures.oddKernel_eq_density line 246
  31. theorem OAI.Erdos970.Erdos970Dependency.MarginalDensityMeasures.odd_lifted_density_measurable line 251
  32. theorem OAI.Erdos970.Erdos970Dependency.MarginalDensityMeasures.even_lifted_density_measurable line 256
  33. theorem OAI.Erdos970.Erdos970Dependency.MarginalDensityMeasures.initialTwoMeasure_eq_density line 261
  34. theorem OAI.Erdos970.Erdos970Dependency.MarginalDensityMeasures.regTwoMeasure_eq_density line 276
  35. theorem OAI.Erdos970.Erdos970Dependency.MarginalDensityMeasures.regThreeMeasure_eq_density line 292
  36. def OAI.Erdos970.Erdos970Dependency.DensityComparison.dominationConstant line 321
  37. theorem OAI.Erdos970.Erdos970Dependency.DensityComparison.dominationConstant_pos line 323
  38. theorem OAI.Erdos970.Erdos970Dependency.DensityComparison.initial_density_le line 326
  39. theorem OAI.Erdos970.Erdos970Dependency.DensityComparison.initial_real_measure_le line 349