OAI/MathematicalPhysics/Boltzmann/Branching/WeightedNetLoss.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Almost-everywhere invariance of the colored forcing along spacetime

  1. abbrev OAI.BoltzmannNonuniqueness.WeightedLocal.spacetimeVolume line 18
  2. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.unstate_congr line 21
  3. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.forcing_congr line 29
  4. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.coldForcing_congr_total line 35
  5. def OAI.BoltzmannNonuniqueness.WeightedLocal.remainderForcing line 42
  6. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.remainderForcing_congr line 46
  7. def OAI.BoltzmannNonuniqueness.WeightedLocal.MildAE line 74

    Source documentation

    The mild identity on every time slice, with spatial null sets allowed to depend on time.

    def MildAE (q b L T : ℝ) (f₀ : JetPrototype.Phase → ℝ)
    (F : ℝ × JetPrototype.Phase → ℝ) : Prop :=
…

    Mentions: OAI.BoltzmannNonuniqueness.JetPrototype.Phase

  8. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.mildAE_of_pointwise line 79
  9. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.slice_congr_spacetime line 84
  10. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.MildAE.representative line 90
  11. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.canonical_mildAE line 100
  12. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.coldForcing_zero line 122
  13. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.coldPicard_zero line 129
  14. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.coldLimit_zero line 138
  15. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.coldForcing_congr_cold line 159
  16. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.finite_coldForcing_le_ae line 174
  17. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.measurable_paste line 224
  18. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.paste_bounds line 229
  19. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.paste_pull line 237
  20. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.paste_mildAE line 242
  21. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.forcing_difference_ae line 298
  22. def OAI.BoltzmannNonuniqueness.WeightedLocal.lossFrequency line 348
  23. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.measurable_lossFrequency line 352
  24. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.lossFrequency_pull line 357
  25. theorem OAI.BoltzmannNonuniqueness.WeightedLocal.lossFrequency_congr line 361
  26. theorem OAI.BoltzmannNonuniqueness.HotRepresentative.hot_net_source_lower line 389