OAI/NumberTheory/Jacobsthal/Analysis/WeightIntegrals.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.NumberTheoryLean.TwoStepDensityBounds.baseRatio line 16
  2. theorem OAI.Erdos970.NumberTheoryLean.TwoStepDensityBounds.baseRatio_valid line 18
  3. theorem OAI.Erdos970.NumberTheoryLean.TwoStepDensityBounds.baseRatio_le line 20
  4. theorem OAI.Erdos970.NumberTheoryLean.TwoStepDensityBounds.valid_of_three_le line 23
  5. theorem OAI.Erdos970.NumberTheoryLean.TwoStepDensityBounds.weight_antitone line 26
  6. theorem OAI.Erdos970.NumberTheoryLean.TwoStepDensityBounds.two_step_density_eq line 35
  7. theorem OAI.Erdos970.NumberTheoryLean.TwoStepDensityBounds.rectangle_admissible line 48
  8. theorem OAI.Erdos970.NumberTheoryLean.TwoStepDensityBounds.W_lower line 59
  9. def OAI.Erdos970.NumberTheoryLean.TwoStepDensityBounds.rectangleLower line 65
  10. theorem OAI.Erdos970.NumberTheoryLean.TwoStepDensityBounds.rectangleLower_pos line 68
  11. theorem OAI.Erdos970.NumberTheoryLean.TwoStepDensityBounds.rectangle_density_lower line 73
  12. def OAI.Erdos970.NumberTheoryLean.TwoStepDensityBounds.minorizationSize line 97
  13. theorem OAI.Erdos970.NumberTheoryLean.TwoStepDensityBounds.minorizationSize_pos line 100
  14. theorem OAI.Erdos970.NumberTheoryLean.TwoStepDensityBounds.minorizationSize_le_one line 103
  15. theorem OAI.Erdos970.NumberTheoryLean.TwoStepDensityBounds.minorizationSize_le_rectangle line 105
  16. def OAI.Erdos970.Erdos970Dependency.WeightIntegrals.wPrimitive line 120
  17. def OAI.Erdos970.Erdos970Dependency.WeightIntegrals.wMass line 121
  18. theorem OAI.Erdos970.Erdos970Dependency.WeightIntegrals.W_continuousAt line 123
  19. theorem OAI.Erdos970.Erdos970Dependency.WeightIntegrals.wPrimitive_deriv line 127
  20. theorem OAI.Erdos970.Erdos970Dependency.WeightIntegrals.wMass_eq line 135
  21. theorem OAI.Erdos970.Erdos970Dependency.WeightIntegrals.wMass_nonneg line 146
  22. theorem OAI.Erdos970.Erdos970Dependency.WeightIntegrals.wMass_mono_right line 151
  23. theorem OAI.Erdos970.Erdos970Dependency.WeightIntegrals.wMass_two_three_lower line 160
  24. theorem OAI.Erdos970.Erdos970Dependency.WeightIntegrals.wMass_initial_upper line 174
  25. def OAI.Erdos970.Erdos970Dependency.WeightIntegrals.tailW line 192
  26. def OAI.Erdos970.Erdos970Dependency.WeightIntegrals.regIntegral line 194
  27. theorem OAI.Erdos970.Erdos970Dependency.WeightIntegrals.tailW_measurable line 196
  28. theorem OAI.Erdos970.Erdos970Dependency.WeightIntegrals.tailW_eq_mass line 200
  29. theorem OAI.Erdos970.Erdos970Dependency.WeightIntegrals.tailW_nonneg line 204
  30. theorem OAI.Erdos970.Erdos970Dependency.WeightIntegrals.tailW_continuousAt line 208
  31. theorem OAI.Erdos970.Erdos970Dependency.WeightIntegrals.regKernel_continuousOn line 213
  32. theorem OAI.Erdos970.Erdos970Dependency.WeightIntegrals.wKernel_intervalIntegrable line 219
  33. theorem OAI.Erdos970.Erdos970Dependency.WeightIntegrals.regIntegral_lower line 226
  34. theorem OAI.Erdos970.Erdos970Dependency.WeightIntegrals.regIntegral_nonneg line 250
  35. theorem OAI.Erdos970.Erdos970Dependency.WeightIntegrals.initial_integral_le line 253