OAI/Analysis/ModularRecovery/Mean.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

The fixed free-ultrafilter mean of symmetric Lebesgue averages and orbit defects.

  1. lemma OAI.BoundedRecovery.StandardModularData.exists_finite_moment_average line 18
  2. lemma OAI.BoundedRecovery.norm_symmetricAverage_le line 90
  3. lemma OAI.BoundedRecovery.tendsto_symmetricAverage_mean line 106
  4. lemma OAI.BoundedRecovery.norm_fixedMean_le line 120
  5. lemma OAI.BoundedRecovery.symmetricAverage_add line 125
  6. lemma OAI.BoundedRecovery.symmetricAverage_smul line 131
  7. lemma OAI.BoundedRecovery.fixedMean_add line 137
  8. lemma OAI.BoundedRecovery.fixedMean_smul line 145
  9. def OAI.BoundedRecovery.meanCLM line 152
  10. lemma OAI.BoundedRecovery.meanCLM_apply line 159
  11. lemma OAI.BoundedRecovery.symmetricAverage_mono line 162
  12. lemma OAI.BoundedRecovery.fixedMean_mono line 170
  13. lemma OAI.BoundedRecovery.symmetricAverage_const line 176
  14. lemma OAI.BoundedRecovery.fixedMean_const line 183
  15. def OAI.BoundedRecovery.translateBCF line 190
  16. lemma OAI.BoundedRecovery.translateBCF_apply line 193
  17. lemma OAI.BoundedRecovery.norm_symmetricAverage_translate_sub_le line 196
  18. lemma OAI.BoundedRecovery.tendsto_symmetricAverage_translate_sub line 218
  19. lemma OAI.BoundedRecovery.fixedMean_translate line 227
  20. lemma OAI.BoundedRecovery.exists_lt_of_lt_fixedMean line 236
  21. def OAI.BoundedRecovery.RealSpectralCalculus.orbitDefect line 254
  22. lemma OAI.BoundedRecovery.RealSpectralCalculus.orbitDefect_apply line 264
  23. lemma OAI.BoundedRecovery.RealSpectralCalculus.norm_orbitDefect_le line 267
  24. lemma OAI.BoundedRecovery.RealSpectralCalculus.orbitDefect_unitary line 275
  25. lemma OAI.BoundedRecovery.RealSpectralCalculus.norm_orbitDefect_sub_le line 281
  26. lemma OAI.BoundedRecovery.RealSpectralCalculus.abs_mean_orbitDefect_sub_le line 297
  27. lemma OAI.BoundedRecovery.RealSpectralCalculus.mean_orbitDefect_nonneg line 306
  28. lemma OAI.BoundedRecovery.RealSpectralCalculus.mean_orbitDefect_le line 313