OAI/MathematicalPhysics/Boltzmann/Jets/OriginMeshStep.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

The actual selected kernel restricted to one origin and a compact scale window

  1. def OAI.BoltzmannNonuniqueness.JetCopyDatum.originScaleRegion line 19
  2. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.originScaleRegion_measurable line 23
  3. def OAI.BoltzmannNonuniqueness.JetCopyDatum.originScaleKernel line 29
  4. instance OAI.BoltzmannNonuniqueness.JetCopyDatum.originScaleKernel_sFinite line 35
  5. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.originScaleKernel_eq_copy line 40
  6. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.originScaleKernel_zero_or_copy line 52
  7. def OAI.BoltzmannNonuniqueness.JetCopyDatum.windowMesh line 87
  8. def OAI.BoltzmannNonuniqueness.JetCopyDatum.meshLabel line 90
  9. def OAI.BoltzmannNonuniqueness.JetCopyDatum.meshLabelRegion line 93
  10. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.meshLabelRegion_measurable line 99
  11. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.meshLabelRegion_originScale line 107
  12. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.meshLabelRegion_disjoint line 113
  13. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.originScale_mem_meshLabel line 124
  14. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.copy_meshLabel_eq line 168
  15. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.originScale_lintegral_eq_mesh_sum line 180
  16. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.meshRegion_lintegral_indicator line 229
  17. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.originScale_step_eq_mesh_sum line 248