OAI/Probability/FreeIsing/Stochastic/SelectedCompensator.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.SelectedCompensator.squareSum line 15
  2. theorem OAI.Problem367.SelectedCompensator.coe_uniformGrid line 21
  3. theorem OAI.Problem367.SelectedCompensator.squareSum_eq_stoppedSum line 28
  4. theorem OAI.Problem367.SelectedCompensator.squareSum_stronglyAdapted line 37
  5. def OAI.Problem367.SelectedCompensator.selected line 53
  6. theorem OAI.Problem367.SelectedCompensator.selected_stronglyAdapted line 56
  7. theorem OAI.Problem367.SelectedCompensator.selected_eq_integral_of_continuous line 65
  8. theorem OAI.Problem367.SelectedCompensator.ae_selected_eq_integral line 73
  9. theorem OAI.Problem367.SelectedCompensator.ae_continuous_selected line 80
  10. theorem OAI.Problem367.SelectedCompensator.selected_zero line 95
  11. theorem OAI.Problem367.SelectedCompensator.abs_squareSum_le line 101
  12. theorem OAI.Problem367.SelectedCompensator.abs_selected_le line 111
  13. theorem OAI.Problem367.SelectedCompensator.squareSum_memLp line 123
  14. theorem OAI.Problem367.SelectedCompensator.selected_memLp line 133
  15. theorem OAI.Problem367.SelectedCompensator.selected_monotone_of_continuous line 144
  16. theorem OAI.Problem367.SelectedCompensator.abs_selected_sub_le line 158
  17. theorem OAI.Problem367.SelectedCompensator.tendsto_squareSum_L1_selected line 175