OAI/Probability/Ballisticity/Estimates/CharacteristicTaylor.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectionalTransience.charPhase line 14
  2. lemma OAI.DirectionalTransience.charPhase_norm line 16
  3. lemma OAI.DirectionalTransience.charPhase_add line 17
  4. def OAI.DirectionalTransience.charTaylorConstant line 20
  5. lemma OAI.DirectionalTransience.charTaylorConstant_nonneg line 21
  6. lemma OAI.DirectionalTransience.charPhase_quadratic_error line 23
  7. lemma OAI.DirectionalTransience.abs_linear_cube_bound line 55
  8. lemma OAI.DirectionalTransience.normalJointPast_complex_weighted_moment_integrable line 82
  9. lemma OAI.DirectionalTransience.normalJointPast_complex_moment line 97
  10. lemma OAI.DirectionalTransience.normalJointPast_complex_mean line 109
  11. lemma OAI.DirectionalTransience.normalJointPast_complex_second line 116
  12. lemma OAI.DirectionalTransience.normalJointPast_complex_cross_integrable line 127
  13. lemma OAI.DirectionalTransience.normalJointPast_complex_cross_bound line 137