OAI/Analysis/StrictMeans/AffineAveraging.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.StrictInverseFirstPower.expScalePoint line 49
  2. lemma OAI.StrictInverseFirstPower.continuous_expScalePoint line 51
  3. lemma OAI.StrictInverseFirstPower.affineProduct_expScale line 54
  4. lemma OAI.StrictInverseFirstPower.halfScale_expScale line 58
  5. lemma OAI.StrictInverseFirstPower.expScale_horizontal line 66
  6. lemma OAI.StrictInverseFirstPower.weighted_scale_periodic line 71
  7. lemma OAI.StrictInverseFirstPower.weighted_scale_bound line 82
  8. def OAI.StrictInverseFirstPower.scaleAverage line 97
  9. lemma OAI.StrictInverseFirstPower.scaleAverage_apply line 103
  10. lemma OAI.StrictInverseFirstPower.scaleAverage_horizontal line 110
  11. lemma OAI.StrictInverseFirstPower.scaleAverage_scale line 120
  12. lemma OAI.StrictInverseFirstPower.scaleAverage_affine line 143
  13. lemma OAI.StrictInverseFirstPower.positiveFunctional_strict line 171
  14. lemma OAI.StrictInverseFirstPower.positiveFunctional_affine_one line 184
  15. lemma OAI.StrictInverseFirstPower.horizontalAverage_monotone line 190
  16. lemma OAI.StrictInverseFirstPower.horizontalAverage_one_pos line 201
  17. lemma OAI.StrictInverseFirstPower.scaleAverage_monotone line 209
  18. lemma OAI.StrictInverseFirstPower.scaleAverage_one_pos line 222
  19. lemma OAI.StrictInverseFirstPower.dyadicExponent_power line 232
  20. lemma OAI.StrictInverseFirstPower.dyadicExponent_pos_iff line 236
  21. theorem OAI.StrictInverseFirstPower.exists_exact_affine_functional line 240
  22. theorem OAI.StrictInverseFirstPower.exists_exact_affine_probability_continuous line 266
  23. def OAI.StrictInverseFirstPower.weightedRebaseMeasure line 285
  24. lemma OAI.StrictInverseFirstPower.measurable_rebase_fixed line 288
  25. lemma OAI.StrictInverseFirstPower.measurable_Qnorm_fixed line 291
  26. instance OAI.StrictInverseFirstPower.weightedRebaseMeasure_isFinite line 294
  27. lemma OAI.StrictInverseFirstPower.weightedRebaseMeasure_integral line 304
  28. lemma OAI.StrictInverseFirstPower.weightedRebaseMeasure_lintegral line 311
  29. lemma OAI.StrictInverseFirstPower.weightedRebaseMeasure_eq_smul line 319
  30. theorem OAI.StrictInverseFirstPower.exists_exact_affine_probability line 335