OAI/Probability/SKGap/Localization/ConditionalModelAlgebra.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKGap.conditionalBlockMatrix line 14
  2. def OAI.SKGap.conditionalMeanCoefficient line 21
  3. def OAI.SKGap.conditionalScalarCoefficient line 26
  4. lemma OAI.SKGap.conditionalCoefficient_add_scalar line 29
  5. lemma OAI.SKGap.conditionalMeanCoefficient_equality line 43
  6. theorem OAI.SKGap.conditional_hessian_rank_form line 53
  7. def OAI.SKGap.conditionalKappa line 137
  8. def OAI.SKGap.conditionalEll line 138
  9. def OAI.SKGap.conditionalMeanData line 140
  10. def OAI.SKGap.conditionalScalarData line 145
  11. def OAI.SKGap.curveKappa line 148
  12. def OAI.SKGap.curveCoefficient line 149
  13. lemma OAI.SKGap.conditionalKappa_curve line 154
  14. lemma OAI.SKGap.curveKappa_sq line 158
  15. lemma OAI.SKGap.conditionalMeanData_curve line 168
  16. lemma OAI.SKGap.continuousAt_conditionalCoefficient line 176
  17. lemma OAI.SKGap.continuousAt_conditionalMeanCoefficient line 193
  18. lemma OAI.SKGap.continuousAt_conditionalScalarCoefficient line 213
  19. lemma OAI.SKGap.continuousAt_conditionalData line 218
  20. lemma OAI.SKGap.continuous_curve_statistics line 254