OAI/Probability/SKFluctuations/ProjectionResidual.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

Projection Residual.

  1. theorem OAI.SKFluctuations.Hierarchy.finite_even_jensen line 19
  2. theorem OAI.SKFluctuations.Hierarchy.finite_centered_even_le line 28
  3. theorem OAI.SKFluctuations.Hierarchy.hierarchyCenteredEvenMoment_le line 53
  4. theorem OAI.SKFluctuations.Hierarchy.integral_segmentLaw_centeredEven_le line 65
  5. theorem OAI.SKFluctuations.Hierarchy.integral_segmentLaw_centeredEven_le_initial line 85
  6. def OAI.SKFluctuations.Hierarchy.segmentResponseCost line 107
  7. theorem OAI.SKFluctuations.Hierarchy.segmentResponseCost_continuous line 116
  8. theorem OAI.SKFluctuations.Hierarchy.segmentResponseCost_bound line 133
  9. theorem OAI.SKFluctuations.Hierarchy.segmentResponseCost_integrable line 146
  10. theorem OAI.SKFluctuations.Hierarchy.segmentMean_mul_score_integrable line 157
  11. theorem OAI.SKFluctuations.Hierarchy.integrable_integral_segmentLaw_cons line 173
  12. theorem OAI.SKFluctuations.Hierarchy.integral_segmentMean_mul_score line 206
  13. theorem OAI.SKFluctuations.Hierarchy.gaussianHierarchyResponse_smul_direction line 313
  14. theorem OAI.SKFluctuations.Hierarchy.hierarchyCenteredEvenMoment_nonneg line 320
  15. theorem OAI.SKFluctuations.Hierarchy.integral_segmentResponseCost_tail_integrable line 327
  16. theorem OAI.SKFluctuations.Hierarchy.integral_segmentResponseCost_cons line 352
  17. def OAI.SKFluctuations.Hierarchy.segmentCenteredEvenMoment line 386
  18. theorem OAI.SKFluctuations.Hierarchy.segmentCenteredEvenMoment_integrable line 391
  19. theorem OAI.SKFluctuations.Hierarchy.segmentCenteredEvenMoment_cons line 402
  20. theorem OAI.SKFluctuations.Hierarchy.segmentCenteredEvenMoment_tail_integrable line 413
  21. theorem OAI.SKFluctuations.Hierarchy.segmentResponseCost_odd_coercivity line 425
  22. theorem OAI.SKFluctuations.Hierarchy.hierarchy_projection_segment line 498
  23. theorem OAI.SKFluctuations.Hierarchy.hierarchy_projection_segment_centered line 552
  24. lemma OAI.SKFluctuations.Hierarchy.quantitative_half_contraction line 576
  25. theorem OAI.SKFluctuations.Hierarchy.hierarchy_projection_segment_half line 593
  26. def OAI.SKFluctuations.Hierarchy.hierarchyClocks line 615
  27. theorem OAI.SKFluctuations.Hierarchy.hierarchyIncrements_eq_scaleDriver line 620
  28. theorem OAI.SKFluctuations.Hierarchy.alignedClock_direction line 633
  29. theorem OAI.SKFluctuations.Hierarchy.alignedClock_variance line 642
  30. theorem OAI.SKFluctuations.Hierarchy.alignedSegment_direction line 648
  31. theorem OAI.SKFluctuations.Hierarchy.alignedSegment_variance line 656