OAI/Probability/ThreeState/Projection.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

Quadratic projections, covariance and truncated correlation estimates.

  1. lemma OAI.ThreeState.symAvg_deviation_mul line 13
  2. lemma OAI.ThreeState.continuous_messageDeviation line 22
  3. lemma OAI.ThreeState.integral_deviation line 25
  4. lemma OAI.ThreeState.integral_deviation_mul line 33
  5. def OAI.ThreeState.edgeDeviationMap line 39
  6. lemma OAI.ThreeState.edge_deviation line 43
  7. lemma OAI.ThreeState.integral_edge_covariance line 48
  8. lemma OAI.ThreeState.integral_edge_deviation_sq line 68
  9. lemma OAI.ThreeState.avg_swap line 78
  10. lemma OAI.ThreeState.avg_add line 81
  11. lemma OAI.ThreeState.avg_mul_const line 84
  12. lemma OAI.ThreeState.avg_const_mul line 87
  13. lemma OAI.ThreeState.avg_covariance_coeff line 90
  14. def OAI.ThreeState.branchSum line 103
  15. lemma OAI.ThreeState.continuous_branchSum line 105
  16. lemma OAI.ThreeState.avg_branchSum line 110
  17. lemma OAI.ThreeState.weighted_deviation_branchSum line 118
  18. lemma OAI.ThreeState.integral_projection_cross line 126
  19. lemma OAI.ThreeState.avg_integral_edge_sq line 152
  20. lemma OAI.ThreeState.integral_projection_variance_coordinate line 165
  21. lemma OAI.ThreeState.integral_projection_variance line 195
  22. lemma OAI.ThreeState.weighted_vector_quadratic line 217
  23. lemma OAI.ThreeState.degree_projection_quadratic line 246
  24. lemma OAI.ThreeState.degree_projection line 264
  25. lemma OAI.ThreeState.truncated_quadratic_lower line 294
  26. def OAI.ThreeState.pairCorrelation line 313
  27. lemma OAI.ThreeState.pairCorrelation_nonneg line 316
  28. lemma OAI.ThreeState.pairCorrelation_lower line 320
  29. lemma OAI.ThreeState.eta_product_lower_control line 336
  30. lemma OAI.ThreeState.pairCorrelation_truncated line 356