OAI/MathematicalPhysics/Boltzmann/Branching/AxisMismatch.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BoltzmannNonuniqueness.AxisMismatch.incoming line 23
2. def OAI.BoltzmannNonuniqueness.AxisMismatch.region line 26
3. theorem OAI.BoltzmannNonuniqueness.AxisMismatch.measurableSet_incoming line 29
4. theorem OAI.BoltzmannNonuniqueness.AxisMismatch.measurableSet_region line 32
5. theorem OAI.BoltzmannNonuniqueness.AxisMismatch.region_eq_restricted line 35
6. theorem OAI.BoltzmannNonuniqueness.AxisMismatch.weight_region_bound line 43
7. theorem OAI.BoltzmannNonuniqueness.AxisMismatch.normalized_region_bound line 98
8. def OAI.BoltzmannNonuniqueness.AxisMismatch.powerValue line 117
9. theorem OAI.BoltzmannNonuniqueness.AxisMismatch.normalized_region_power_bound line 121
10. theorem OAI.BoltzmannNonuniqueness.AxisMismatch.power_tendsto_zero line 153
11. theorem OAI.BoltzmannNonuniqueness.AxisMismatch.uniform_axis_mismatch line 166

    Source documentation

    The full axial-mismatch limit, uniform in the output axial velocity.

    theorem uniform_axis_mismatch {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 (incoming v δ ×ˢ univ) ≤ ENNReal.ofReal ε := by
    …

    Mentions: OAI.BoltzmannNonuniqueness.Velocity, OAI.BoltzmannNonuniqueness.AxisMismatch.incoming