OAI/Probability/FreeIsing/Estimates/FiniteIsingCompensatedSquare.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem367.FiniteIsingFiltering.quadraticCompensator line 15
2. theorem OAI.Problem367.FiniteIsingFiltering.quadraticCompensator_eq_selected line 20
3. theorem OAI.Problem367.FiniteIsingFiltering.stronglyAdapted_quadraticCompensator line 32
4. theorem OAI.Problem367.FiniteIsingFiltering.quadraticCompensator_eq_integral_energy line 47
5. theorem OAI.Problem367.FiniteIsingFiltering.mean_compensatedSquare_martingale line 60
6. theorem OAI.Problem367.FiniteIsingFiltering.mean_compensatedSquare_energy_martingale line 96