OAI/Geometry/CAT0Fillings/Chord/Fubini.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CAT0Fillings.secant_lower_bound line 13
  2. theorem OAI.CAT0Fillings.chord_scalar_bound line 46
  3. def OAI.CAT0Fillings.ChordTransform.kernel line 124
  4. lemma OAI.CAT0Fillings.ChordTransform.kernel_pos line 126
  5. lemma OAI.CAT0Fillings.ChordTransform.kernel_le_one line 129
  6. lemma OAI.CAT0Fillings.ChordTransform.kernel_hasDerivAt line 133
  7. lemma OAI.CAT0Fillings.ChordTransform.kernel_deriv_bound line 142
  8. lemma OAI.CAT0Fillings.ChordTransform.kernel_lipschitzOn line 150
  9. lemma OAI.CAT0Fillings.ChordTransform.kernel_slope_bound line 157
  10. def OAI.CAT0Fillings.ChordTransform.transform line 167
  11. lemma OAI.CAT0Fillings.ChordTransform.kernel_aestronglyMeasurable line 171
  12. lemma OAI.CAT0Fillings.ChordTransform.kernel_integrable line 175
  13. lemma OAI.CAT0Fillings.ChordTransform.transform_zero line 183
  14. lemma OAI.CAT0Fillings.ChordTransform.transform_nonneg line 188
  15. lemma OAI.CAT0Fillings.ChordTransform.transform_pos line 192
  16. lemma OAI.CAT0Fillings.ChordTransform.transform_lipschitzOn line 205
  17. lemma OAI.CAT0Fillings.ChordTransform.transform_hasDerivAt line 225
  18. lemma OAI.CAT0Fillings.ChordTransform.transform_hasDerivWithinAt_zero line 244
  19. def OAI.CAT0Fillings.ChordAverage.average line 280
  20. lemma OAI.CAT0Fillings.ChordAverage.integrable_weight line 283
  21. lemma OAI.CAT0Fillings.ChordAverage.weight_integral line 287
  22. lemma OAI.CAT0Fillings.ChordAverage.integrable_weighted line 292
  23. lemma OAI.CAT0Fillings.ChordAverage.integrable_average line 299
  24. lemma OAI.CAT0Fillings.ChordAverage.average_zero line 308
  25. lemma OAI.CAT0Fillings.ChordAverage.average_rescale line 313
  26. lemma OAI.CAT0Fillings.ChordAverage.weighted_continuousOn line 339
  27. lemma OAI.CAT0Fillings.ChordAverage.average_hasDerivAt line 344
  28. lemma OAI.CAT0Fillings.ChordAverage.average_ode line 371
  29. lemma OAI.CAT0Fillings.ChordAverage.average_pos line 377
  30. lemma OAI.CAT0Fillings.ChordAverage.mul_weight line 398
  31. lemma OAI.CAT0Fillings.ChordAverage.average_hasDerivWithinAt_zero line 404
  32. theorem OAI.CAT0Fillings.ChordTransform.distribution_bound line 490
  33. lemma OAI.CAT0Fillings.ChordIdentity.rpow_shift_one line 541
  34. lemma OAI.CAT0Fillings.ChordIdentity.rpow_shift_two line 544
  35. lemma OAI.CAT0Fillings.ChordIdentity.scalar_antiderivative line 547
  36. lemma OAI.CAT0Fillings.ChordIdentity.integral_weighted_kernel line 567
  37. theorem OAI.CAT0Fillings.ChordIdentity.scalar_identity line 576
  38. lemma OAI.CAT0Fillings.ChordTransform.weighted_kernel_prod_integrable line 608
  39. theorem OAI.CAT0Fillings.ChordTransform.average_transform line 634
  40. theorem OAI.CAT0Fillings.ChordTransform.average_transform_scalar_identity line 650