OAI/Probability/FreeIsing/Posterior/FilteringRepresentationClosure.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem367.FilteringRepresentationClosure.eq_of_cross_energy line 16
  2. theorem OAI.Problem367.FilteringRepresentationClosure.cross_energy_of_approximations line 24
  3. theorem OAI.Problem367.FilteringRepresentationClosure.eq_of_approximations_and_energy line 36
  4. theorem OAI.Problem367.FilteringRepresentationClosure.norm_finset_sum_sq line 49
  5. theorem OAI.Problem367.FilteringRepresentationClosure.norm_residual_sq_eq_sub_sum line 64
  6. theorem OAI.Problem367.FilteringRepresentationClosure.norm_residual_sq_eq_tsum_compl line 73
  7. theorem OAI.Problem367.FilteringRepresentationClosure.hasSum_of_orthogonal_cross_energy line 88
  8. theorem OAI.Problem367.FilteringRepresentationClosure.ae_eq_of_cross_second_moment line 113
  9. theorem OAI.Problem367.FilteringRepresentationClosure.tendsto_toLp_of_integral_sq_error line 122
  10. theorem OAI.Problem367.FilteringRepresentationClosure.integral_mul_eq_of_meanSquare_limit line 134
  11. theorem OAI.Problem367.FilteringRepresentationClosure.tendsto_integral_sq_fintype_sum_error line 147
  12. theorem OAI.Problem367.FilteringRepresentationClosure.ae_eq_of_approximations_and_energy line 170
  13. theorem OAI.Problem367.FilteringRepresentationClosure.integral_sq_residual_eq_tsum_compl line 191
  14. theorem OAI.Problem367.FilteringRepresentationClosure.hasSum_toLp_of_cross_energy line 216
  15. theorem OAI.Problem367.FilteringRepresentationClosure.ae_eq_fintype_sum_of_cross_energy line 232
  16. theorem OAI.Problem367.FilteringRepresentationClosure.tendsto_integral_sq_residual line 247