OAI/Analysis/ModularRecovery/FiniteMoments.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Simultaneous finite approximations of modular moments.

  1. lemma OAI.BoundedRecovery.norm_sum_probability_smul_le line 15
  2. lemma OAI.BoundedRecovery.StandardModularData.real_smul_mem line 33
  3. def OAI.BoundedRecovery.StandardModularData.modularAverage line 39
  4. lemma OAI.BoundedRecovery.StandardModularData.modularAverage_mem line 42
  5. lemma OAI.BoundedRecovery.StandardModularData.norm_modularAverage_le line 46
  6. lemma OAI.BoundedRecovery.StandardModularData.modularAverage_apply_xi line 51
  7. lemma OAI.BoundedRecovery.StandardModularData.norm_modularAverage_apply_xi_sub_le line 55
  8. lemma OAI.BoundedRecovery.StandardModularData.modularAverage_sandwich line 65
  9. lemma OAI.BoundedRecovery.StandardModularData.averageSquare_eq line 71
  10. lemma OAI.BoundedRecovery.StandardModularData.averageReverseSquare_eq line 76
  11. lemma OAI.BoundedRecovery.StandardModularData.isSelfAdjoint_averageSquare line 81
  12. lemma OAI.BoundedRecovery.StandardModularData.re_inner_operator_le_of_small line 86