OAI/NumberTheory/Jacobsthal/Estimates/WeightedMonotoneBound.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos970.ErdosMonotoneQuadrature.nonnegative_layercake_discrepancy line 15
  2. theorem OAI.Erdos970.ErdosMonotoneQuadrature.integrable_layercake_discrepancy line 55
  3. theorem OAI.Erdos970.ErdosMonotoneQuadrature.monotone_level_orderConnected line 83
  4. theorem OAI.Erdos970.ErdosMonotoneQuadrature.nonnegative_monotone_integral_discrepancy line 94
  5. def OAI.Erdos970.ErdosMonotoneQuadrature.reciprocalWeight line 135
  6. theorem OAI.Erdos970.ErdosMonotoneQuadrature.reciprocalWeight_pos line 137
  7. theorem OAI.Erdos970.ErdosMonotoneQuadrature.reciprocalWeight_le line 140
  8. theorem OAI.Erdos970.ErdosMonotoneQuadrature.reciprocalWeight_continuous line 143
  9. theorem OAI.Erdos970.ErdosMonotoneQuadrature.reciprocalWeight_antitone line 147
  10. theorem OAI.Erdos970.ErdosMonotoneQuadrature.reciprocalWeight_eq line 152
  11. def OAI.Erdos970.ErdosMonotoneQuadrature.reciprocalMeasure line 155
  12. theorem OAI.Erdos970.ErdosMonotoneQuadrature.reciprocalMeasure_finite line 158
  13. theorem OAI.Erdos970.ErdosMonotoneQuadrature.reciprocalMeasure_integral line 166
  14. theorem OAI.Erdos970.ErdosMonotoneQuadrature.reciprocalMeasure_real line 174
  15. theorem OAI.Erdos970.ErdosMonotoneQuadrature.reciprocalMeasure_discrepancy line 180
  16. theorem OAI.Erdos970.ErdosMonotoneQuadrature.signed_monotone_integral_discrepancy line 200
  17. theorem OAI.Erdos970.ErdosMonotoneQuadrature.weighted_monotone_discrepancy line 254
  18. theorem OAI.Erdos970.ErdosMonotoneQuadrature.weighted_from_all_endpoint_intervals line 285