OAI/Probability/SpanningForest/TiltResponse.lean
8 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.Problem336.TiltResponse.covline 16 - lemma
OAI.Problem336.TiltResponse.mean_const_mulline 19 - lemma
OAI.Problem336.TiltResponse.mean_sumline 26 - lemma
OAI.Problem336.TiltResponse.cov_const_mul_rightline 31 - lemma
OAI.Problem336.TiltResponse.cov_sum_rightline 38 - theorem
OAI.Problem336.TiltResponse.mean_sub_le_of_cov_leline 43 - theorem
OAI.Problem336.TiltResponse.cov_direction_leline 54 - theorem
OAI.Problem336.TiltResponse.mean_sub_le_of_covariance_rowline 64