OAI/MathematicalPhysics/Boltzmann/Branching/ChartPointLift.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

The normalized gain as a measure on chart coordinates

This measure retains the incoming velocity and both plane coordinates. Its restriction equals the chart gain, so countable shell estimates concern the full normalized kernel of the manuscript.

  1. abbrev OAI.BoltzmannNonuniqueness.ChartKernel.Coordinates line 24
  2. theorem OAI.BoltzmannNonuniqueness.ChartKernel.measurable_transverse line 26
  3. theorem OAI.BoltzmannNonuniqueness.ChartKernel.measurable_axial line 29
  4. theorem OAI.BoltzmannNonuniqueness.ChartKernel.measurable_point line 32
  5. theorem OAI.BoltzmannNonuniqueness.ChartKernel.measurable_H line 48
  6. theorem OAI.BoltzmannNonuniqueness.ChartKernel.measurable_W line 52
  7. def OAI.BoltzmannNonuniqueness.ChartKernel.density line 56
  8. theorem OAI.BoltzmannNonuniqueness.ChartKernel.measurable_density line 59
  9. def OAI.BoltzmannNonuniqueness.ChartKernel.measure line 66
  10. theorem OAI.BoltzmannNonuniqueness.ChartKernel.region_eq_measure line 70
  11. def OAI.BoltzmannNonuniqueness.ChartKernel.normalizedMeasure line 93
  12. theorem OAI.BoltzmannNonuniqueness.ChartKernel.normalized_region_eq line 96
  13. theorem OAI.BoltzmannNonuniqueness.ChartKernel.total_eq line 101
  14. theorem OAI.BoltzmannNonuniqueness.ChartKernel.normalized_total_eq line 107
  15. theorem OAI.BoltzmannNonuniqueness.ChartKernel.measure_mono_incoming line 111
  16. theorem OAI.BoltzmannNonuniqueness.ChartKernel.measure_smul line 119
  17. theorem OAI.BoltzmannNonuniqueness.ChartKernel.measure_add line 125
  18. theorem OAI.BoltzmannNonuniqueness.ChartKernel.measure_withDensity line 131
  19. theorem OAI.BoltzmannNonuniqueness.ChartKernel.restriction_comparison line 139

    Source documentation

    A pointwise comparison, integrated without losing the coordinate restriction.

    theorem restriction_comparison (c : Measure Velocity) {w h k : Velocity → ℝ≥0∞}
    (hw : Measurable w) (hk : Measurable k) (v : Velocity) (a : ℝ≥0∞)
    {S T : Set Coordinates} (hS : MeasurableSet S) (hT : MeasurableSet T)
    (hp : ∀ y, S.indicator (density h v) y ≤
      a * (w y.1 * T.indicator (density k v) y)) :
    measure c h v S ≤ a * measure (c.withDensity w) k v T := by
…

    Mentions: OAI.BoltzmannNonuniqueness.Velocity, OAI.BoltzmannNonuniqueness.ChartKernel.Coordinates, OAI.BoltzmannNonuniqueness.ChartKernel.density, OAI.BoltzmannNonuniqueness.ChartKernel.measure

  20. theorem OAI.BoltzmannNonuniqueness.ChartKernel.measure_restrict_incoming line 156
  21. theorem OAI.BoltzmannNonuniqueness.ChartKernel.normalized_restrict_incoming line 162
  22. theorem OAI.BoltzmannNonuniqueness.ChartKernel.measurable_joint_point line 184
  23. theorem OAI.BoltzmannNonuniqueness.ChartKernel.measurable_joint_normalized_density line 197
  24. theorem OAI.BoltzmannNonuniqueness.ChartKernel.measurable_lifted_density line 222
  25. theorem OAI.BoltzmannNonuniqueness.ChartKernel.measurable_lifted_point line 229