OAI/Analysis/IntegralMeans/AffineLaw.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Brennan.positiveFunctionalCLM line 25
  2. def OAI.Brennan.intervalFunctional line 29
  3. lemma OAI.Brennan.intervalFunctional_apply line 50
  4. lemma OAI.Brennan.intervalFunctional_nonneg line 58
  5. def OAI.Brennan.pointOperator line 67
  6. lemma OAI.Brennan.pointOperator_mul line 69
  7. lemma OAI.Brennan.pointOperator_zero_one line 73
  8. lemma OAI.Brennan.pointOperator_horizontal line 79
  9. lemma OAI.Brennan.transfer_endpoint_step line 81
  10. lemma OAI.Brennan.transfer_endpoint line 97
  11. lemma OAI.Brennan.endpoint_norm_bound line 110
  12. lemma OAI.Brennan.eigenfunctional_pow line 133
  13. lemma OAI.Brennan.eigenfunctional_horizontal_period line 140
  14. lemma OAI.Brennan.positive_functional_strict line 177
  15. def OAI.Brennan.probabilityFunctional line 186
  16. lemma OAI.Brennan.probabilityFunctional_apply line 195
  17. lemma OAI.Brennan.probabilityFunctional_one line 199
  18. lemma OAI.Brennan.probabilityFunctional_pos line 203
  19. lemma OAI.Brennan.periodic_dyadic_integral line 207
  20. lemma OAI.Brennan.continuous_pointOperator_x line 224
  21. lemma OAI.Brennan.continuous_horizontalOperator line 228
  22. def OAI.Brennan.horizontalAverage line 231
  23. lemma OAI.Brennan.horizontalAverage_apply line 236
  24. lemma OAI.Brennan.horizontalAverage_nonneg line 239
  25. lemma OAI.Brennan.horizontalAverage_mass_pos line 245
  26. lemma OAI.Brennan.functional_point_periodic line 257
  27. lemma OAI.Brennan.horizontalAverage_point line 266
  28. lemma OAI.Brennan.horizontalAverage_invariant line 278
  29. lemma OAI.Brennan.horizontalAverage_half_scale line 289
  30. lemma OAI.Brennan.period_average_invariant line 315
  31. lemma OAI.Brennan.intervalFunctional_mass_pos line 335
  32. def OAI.Brennan.logScaledOperator line 350
  33. lemma OAI.Brennan.logScaledOperator_apply line 353
  34. lemma OAI.Brennan.continuous_logScaledOperator line 356
  35. lemma OAI.Brennan.logScaledOperator_pos line 362
  36. lemma OAI.Brennan.logScaledOperator_zero line 367
  37. lemma OAI.Brennan.logScaledOperator_add line 370
  38. lemma OAI.Brennan.logScaledOperator_horizontal line 374
  39. lemma OAI.Brennan.horizontalAverage_log_period line 380
  40. def OAI.Brennan.scaleAverage line 396
  41. lemma OAI.Brennan.scaleAverage_apply line 401
  42. lemma OAI.Brennan.scaleAverage_pos line 405
  43. lemma OAI.Brennan.scaleAverage_mass_pos line 410
  44. lemma OAI.Brennan.scaleAverage_covariant line 414
  45. lemma OAI.Brennan.scaleAverage_horizontal line 431
  46. def OAI.Brennan.transferRho line 442
  47. def OAI.Brennan.transferBeta line 444
  48. lemma OAI.Brennan.transferBeta_gt_one line 446
  49. lemma OAI.Brennan.exists_weighted_continuous_law line 451
  50. lemma OAI.Brennan.weighted_measure_eq line 491
  51. lemma OAI.Brennan.weighted_lintegral_of_continuous line 510