OAI/MathematicalPhysics/Boltzmann/Branching/AxisInput.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Geometric exclusion of the axis for a nearly axial incoming sheet

Small transverse incoming velocity and small axial mismatch force the collision plane away from the transverse origin. This is the geometric part of the off-axis small-input estimate in Section 3.

  1. theorem OAI.BoltzmannNonuniqueness.AxisGeometry.normal_lower_bound line 25
  2. theorem OAI.BoltzmannNonuniqueness.AxisGeometry.plane_offset_lower_bound line 32
  3. theorem OAI.BoltzmannNonuniqueness.AxisGeometry.transverse_plane_exclusion line 47
  4. theorem OAI.BoltzmannNonuniqueness.AxisGeometry.chart_exclusion line 76
  5. def OAI.BoltzmannNonuniqueness.AxisInput.away line 112
  6. def OAI.BoltzmannNonuniqueness.AxisInput.awayBall line 115
  7. theorem OAI.BoltzmannNonuniqueness.AxisInput.measurableSet_away line 117
  8. theorem OAI.BoltzmannNonuniqueness.AxisInput.measurableSet_awayBall line 120
  9. theorem OAI.BoltzmannNonuniqueness.AxisInput.weight_bound line 123
  10. theorem OAI.BoltzmannNonuniqueness.AxisInput.weight_awayBall_le line 131
  11. theorem OAI.BoltzmannNonuniqueness.AxisInput.normalized_awayBall_bound line 153
  12. def OAI.BoltzmannNonuniqueness.AxisInput.powerConstant line 180
  13. theorem OAI.BoltzmannNonuniqueness.AxisInput.powerConstant_nonneg line 184
  14. theorem OAI.BoltzmannNonuniqueness.AxisInput.normalized_awayBall_power_bound line 192
  15. theorem OAI.BoltzmannNonuniqueness.AxisInput.power_tendsto_zero line 219
  16. theorem OAI.BoltzmannNonuniqueness.AxisInput.uniform_axis_input line 229

    Source documentation

    The first axis-input limit, with the output-speed restriction unnecessary.

    theorem uniform_axis_input {q L δ ε : ℝ} (hq₁ : 1 < q) (hq₂ : q < 2)
    (hδ : 0 < δ) (hε : 0 < ε) :
    ∃ η : ℝ, 0 < η ∧ ∀ (d : ℝ) (ρ : Measure ℝ) (_ : IsProbabilityMeasure ρ)
      (_ : 0 ≤ d) (_ : d ≤ 1 / 8) (_ : AxialMoment ρ L)
      (v : Velocity) (_ : transverse v ≠ 0) (_ : ‖transverse v‖ ≤ η),
      normalizedMeasure (sheetLaw d ρ) q v (away v δ) ≤ ENNReal.ofReal ε := by
…

    Mentions: OAI.BoltzmannNonuniqueness.Velocity, OAI.BoltzmannNonuniqueness.AxisInput.away