OAI/Probability/FreeIsing/Conditioning/ShiftedLoss.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem367.shiftedLossCoefficient line 11
2. lemma OAI.Problem367.shiftedLossCoefficient_pos line 15
3. lemma OAI.Problem367.integral_shifted_attenuation_loss_explicit line 20
4. lemma OAI.Problem367.ae_condDistrib_abs_le line 48
5. lemma OAI.Problem367.condExp_shifted_attenuation_le_condDistrib_variance line 56
6. lemma OAI.Problem367.condDistrib_variance_eq_condExp_sq_sub line 83
7. lemma OAI.Problem367.condExp_shifted_attenuation_le_condVariance line 101