OAI/Probability/SKValue/Processes/MeshRaw.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKValue.meshRaw line 25
  2. def OAI.SKValue.meshTerminal line 29
  3. def OAI.SKValue.meshA line 32
  4. def OAI.SKValue.meshB line 38
  5. def OAI.SKValue.finiteShiftedValue line 42
  6. lemma OAI.SKValue.mesh_time_mem line 45
  7. lemma OAI.SKValue.mesh_terminal_measurable line 52
  8. lemma OAI.SKValue.mesh_raw_measurable line 59
  9. lemma OAI.SKValue.mesh_raw_depends line 66
  10. lemma OAI.SKValue.mesh_terminal_depends line 70
  11. lemma OAI.SKValue.mesh_raw_memLp line 74
  12. lemma OAI.SKValue.mesh_coefficient_errors line 84
  13. lemma OAI.SKValue.mesh_coefficients_norms line 102
  14. lemma OAI.SKValue.mesh_leading_norm line 107
  15. lemma OAI.SKValue.abs_sqrt_sub_one_le line 131