OAI/Analysis/StrictMeans/HorizontalAveraging.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.StrictInverseFirstPower.compactTest_integrable line 46
  2. def OAI.StrictInverseFirstPower.probabilityFunctional line 49
  3. lemma OAI.StrictInverseFirstPower.probabilityFunctional_apply line 58
  4. lemma OAI.StrictInverseFirstPower.probabilityFunctional_monotone line 61
  5. lemma OAI.StrictInverseFirstPower.probabilityFunctional_one line 64
  6. lemma OAI.StrictInverseFirstPower.eigenfunctional_power line 67
  7. instance OAI.StrictInverseFirstPower.diskFamilyMeasurableSpace line 75
  8. instance OAI.StrictInverseFirstPower.(instance at line 76) line 76
  9. def OAI.StrictInverseFirstPower.dyadicLogGrowth line 78
  10. def OAI.StrictInverseFirstPower.dyadicRadius line 79
  11. def OAI.StrictInverseFirstPower.dyadicExponent line 80
  12. lemma OAI.StrictInverseFirstPower.dyadicRadius_pos line 82
  13. lemma OAI.StrictInverseFirstPower.dyadicLogGrowth_nonneg line 83
  14. lemma OAI.StrictInverseFirstPower.dyadicExponent_nonneg line 85
  15. theorem OAI.StrictInverseFirstPower.exists_dyadic_eigenfunctional line 88
  16. lemma OAI.StrictInverseFirstPower.eigenfunctional_horizontal_period line 96
  17. lemma OAI.StrictInverseFirstPower.continuous_xyPoint line 135
  18. lemma OAI.StrictInverseFirstPower.continuous_horizontalPoint line 140
  19. lemma OAI.StrictInverseFirstPower.affineProduct_horizontal line 143
  20. lemma OAI.StrictInverseFirstPower.affineProduct_horizontal_xy line 147
  21. lemma OAI.StrictInverseFirstPower.affineProduct_xy_horizontal line 151
  22. lemma OAI.StrictInverseFirstPower.continuous_functional_affine line 155
  23. lemma OAI.StrictInverseFirstPower.affineOperator_compact_bound line 159
  24. def OAI.StrictInverseFirstPower.intervalFunctional line 176
  25. lemma OAI.StrictInverseFirstPower.intervalFunctional_apply line 200
  26. def OAI.StrictInverseFirstPower.affineIntervalFunctional line 204
  27. lemma OAI.StrictInverseFirstPower.affineIntervalFunctional_apply line 210
  28. def OAI.StrictInverseFirstPower.horizontalAverage line 214
  29. lemma OAI.StrictInverseFirstPower.horizontalAverage_apply line 217
  30. lemma OAI.StrictInverseFirstPower.functional_horizontal_periodic line 220
  31. lemma OAI.StrictInverseFirstPower.horizontalAverage_invariant line 230
  32. def OAI.StrictInverseFirstPower.halfScalePoint line 255
  33. lemma OAI.StrictInverseFirstPower.dyadicLeft_eq_horizontal_scale line 257
  34. lemma OAI.StrictInverseFirstPower.dyadicRight_eq_horizontal_scale line 263
  35. lemma OAI.StrictInverseFirstPower.horizontal_dyadicLeft line 269
  36. lemma OAI.StrictInverseFirstPower.horizontal_dyadicRight line 276
  37. lemma OAI.StrictInverseFirstPower.affineOperator_horizontal_dyadic line 283
  38. lemma OAI.StrictInverseFirstPower.periodic_integral_double line 290
  39. lemma OAI.StrictInverseFirstPower.horizontalAverage_eigen line 301
  40. lemma OAI.StrictInverseFirstPower.horizontally_invariant_dyadic line 319
  41. lemma OAI.StrictInverseFirstPower.horizontalAverage_halfScale line 328