OAI/Analysis/Steinitz/Survival.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

Gaussian path survival with slab and state constraints.

  1. def OAI.GaussianEvents.constraints line 16
  2. lemma OAI.GaussianEvents.constraints_closed line 20
  3. lemma OAI.GaussianEvents.constraints_convex line 25
  4. lemma OAI.GaussianEvents.constraints_symmetric line 32
  5. lemma OAI.GaussianEvents.finite_half line 37
  6. lemma OAI.GaussianAR.epoch_survival line 69
  7. def OAI.EuclideanSteinitz.Filter.epochFactor line 149
  8. def OAI.EuclideanSteinitz.Filter.momentConstant line 150
  9. def OAI.EuclideanSteinitz.Filter.survivalRadius line 151
  10. lemma OAI.EuclideanSteinitz.Filter.epochFactor_ge_one line 153
  11. lemma OAI.EuclideanSteinitz.Filter.momentConstant_ge line 156
  12. lemma OAI.EuclideanSteinitz.Filter.survivalRadius_pos line 159
  13. lemma OAI.EuclideanSteinitz.Filter.squareMass_sub_comm line 164
  14. lemma OAI.EuclideanSteinitz.Filter.filtered_epoch_survival line 173
  15. lemma OAI.EuclideanSteinitz.Filter.state_scale line 280
  16. lemma OAI.EuclideanSteinitz.Filter.sum_scale_size line 290
  17. lemma OAI.EuclideanSteinitz.Filter.form_mono line 299
  18. lemma OAI.EuclideanSteinitz.Filter.cutoff_cover line 304
  19. lemma OAI.EuclideanSteinitz.Filter.lift_gram line 328
  20. lemma OAI.EuclideanSteinitz.Filter.norm_sq_reconstruct line 336
  21. lemma OAI.EuclideanSteinitz.Filter.exists_finite_scales line 352
  22. lemma OAI.GaussianEvents.finite_exp line 378
  23. def OAI.GaussianAR.slabRadius line 397
  24. lemma OAI.GaussianAR.slabRadius_pos line 398
  25. lemma OAI.GaussianAR.weighted_diagonal_eq line 400
  26. lemma OAI.GaussianAR.one_slab_survival line 410
  27. lemma OAI.GaussianAR.slabs_survival line 427
  28. def OAI.EuclideanSteinitz.Filter.stateRadius line 457
  29. def OAI.EuclideanSteinitz.Filter.stateRate line 458
  30. lemma OAI.EuclideanSteinitz.Filter.stateRadius_pos line 459
  31. lemma OAI.EuclideanSteinitz.Filter.stateRate_nonneg line 460
  32. lemma OAI.EuclideanSteinitz.Filter.matrixMap_mul_apply line 463
  33. lemma OAI.EuclideanSteinitz.Filter.reconstruction_bound line 469
  34. lemma OAI.EuclideanSteinitz.Filter.state_survival line 500
  35. def OAI.GaussianAR.pathMatrix line 587
  36. lemma OAI.GaussianAR.pathMatrix_det line 590
  37. lemma OAI.GaussianAR.pathMatrix_det_pos line 620
  38. lemma OAI.GaussianAR.evaluation_apply line 626
  39. lemma OAI.GaussianAR.pathMatrix_apply line 636
  40. lemma OAI.GaussianAR.path_initial line 641
  41. lemma OAI.GaussianAR.path_step line 647
  42. lemma OAI.GaussianAR.pathMatrix_lin_det line 659
  43. def OAI.GaussianAR.pathEquiv line 663
  44. lemma OAI.GaussianAR.pathEquiv_apply line 669
  45. lemma OAI.GaussianAR.pathEquiv_symm_initial line 675
  46. lemma OAI.GaussianAR.pathEquiv_symm_step line 683
  47. lemma OAI.GaussianAR.pathEquiv_det line 693
  48. lemma OAI.GaussianAR.transition_scalar line 708
  49. lemma OAI.GaussianAR.reciprocal_rate line 749