OAI/Probability/FreeIsing/Gaussian/TreeResponsePlanted.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem367.GaussianTreeResponse.spinDrift line 14
2. lemma OAI.Problem367.GaussianTreeResponse.measurable_spinDrift line 17
3. def OAI.Problem367.GaussianTreeResponse.observedRow line 21
4. lemma OAI.Problem367.GaussianTreeResponse.observedRow_eq_shiftedRow line 26
5. lemma OAI.Problem367.GaussianTreeResponse.hasLaw_restrict_noise line 40
6. lemma OAI.Problem367.GaussianTreeResponse.integrable_observedRow_sq line 61
7. theorem OAI.Problem367.GaussianTreeResponse.integral_observedRow_sq_le line 77
8. theorem OAI.Problem367.GaussianTreeResponse.integral_observedRow_energy_le line 94
9. theorem OAI.Problem367.GaussianTreeResponse.integral_observedRow_energy_tail_le line 110