OAI/Probability/SpanningForest/USTResponse.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Problem336.USTResponse.TreeSample line 11
  2. abbrev OAI.Problem336.USTResponse.FiniteEdge line 14
  3. def OAI.Problem336.USTResponse.indicator line 17
  4. lemma OAI.Problem336.USTResponse.tree_property line 20
  5. lemma OAI.Problem336.USTResponse.indicator_binary line 24
  6. lemma OAI.Problem336.USTResponse.sum_indicator line 29
  7. def OAI.Problem336.USTResponse.weight line 42
  8. def OAI.Problem336.USTResponse.partition line 45
  9. def OAI.Problem336.USTResponse.mass line 48
  10. lemma OAI.Problem336.USTResponse.weight_pos line 51
  11. lemma OAI.Problem336.USTResponse.partition_pos line 54
  12. lemma OAI.Problem336.USTResponse.mass_nonneg line 59
  13. lemma OAI.Problem336.USTResponse.sum_mass line 63
  14. def OAI.Problem336.USTResponse.inclusion line 68
  15. def OAI.Problem336.USTResponse.edgeCovariance line 71
  16. lemma OAI.Problem336.USTResponse.weight_zero line 75
  17. lemma OAI.Problem336.USTResponse.partition_zero line 78
  18. lemma OAI.Problem336.USTResponse.mass_zero line 82
  19. lemma OAI.Problem336.USTResponse.inclusion_eq_ratio line 86
  20. lemma OAI.Problem336.USTResponse.inclusion_zero line 92
  21. lemma OAI.Problem336.USTResponse.inclusion_zero_eq_ustCylinder line 102
  22. lemma OAI.Problem336.USTResponse.inclusion_nonneg line 109
  23. lemma OAI.Problem336.USTResponse.inclusion_le_one line 115
  24. lemma OAI.Problem336.USTResponse.sum_edgeCovariance_eq_zero line 122
  25. theorem OAI.Problem336.USTResponse.abs_covariance_row line 128
  26. theorem OAI.Problem336.USTResponse.abs_covariance_row_le_half line 137
  27. lemma OAI.Problem336.USTResponse.inclusion_eq_gibbs_mean line 145
  28. lemma OAI.Problem336.USTResponse.edgeCovariance_eq_gibbs_covariance line 151
  29. theorem OAI.Problem336.USTResponse.hasDerivAt_inclusion_direction line 159
  30. theorem OAI.Problem336.USTResponse.inclusion_response line 168
  31. theorem OAI.Problem336.USTResponse.inclusion_response_of_coordinate_bound line 181
  32. lemma OAI.Problem336.USTResponse.continuous_inclusion line 191
  33. lemma OAI.Problem336.USTResponse.measurable_inclusion line 198