OAI/MathematicalPhysics/Boltzmann/Approximation/MildCharacteristics.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.BoltzmannNonuniqueness.PositiveIntegral.value_along_flight line 20
2. theorem OAI.BoltzmannNonuniqueness.PositiveIntegral.weak_characteristic line 36

   Source documentation

   The integral form of the transport equation, along almost every characteristic. The source is only required to be measurable and bounded.

   theorem weak_characteristic {T L S : ℝ} (hT : 0 ≤ T)
       {f₀ : JetPrototype.Phase → ℝ} (hf₀ : Measurable f₀)
       {F g : ℝ × JetPrototype.Phase → ℝ} (hFm : Measurable F) (hgm : Measurable g)
       (hg : ∀ z, |g z| ≤ S)
       (hmild : ∀ t ∈ Icc 0 T, (fun p => F (t,p)) =ᵐ[FlightMeasure.phaseVolume]
         (fun p => value T L JetBarrier.flight f₀ g (t,p)))
       {ψ ψ' : ℝ → ℝ} (hψ : ContinuousOn ψ (Icc 0 T))
       (hψ' : ContinuousOn ψ' (Icc 0 T))
       (hdψ : ∀ t ∈ Icc 0 T, HasDerivAt ψ (ψ' t) t) :
       ∀ᵐ p ∂FlightMeasure.phaseVolume,
         (∫ t in 0..T, ψ' t*F (t,JetBarrier.flight t p) +
           ψ t*(g (t,JetBarrier.flight t p)-L*F (t,JetBarrier.flight t p))) =
   …

   Mentions: OAI.BoltzmannNonuniqueness.JetPrototype.Phase, OAI.BoltzmannNonuniqueness.FlightMeasure.phaseVolume, OAI.BoltzmannNonuniqueness.PositiveIntegral.value, OAI.BoltzmannNonuniqueness.JetBarrier.flight

3. def OAI.BoltzmannNonuniqueness.MildStability.value line 108
4. theorem OAI.BoltzmannNonuniqueness.MildStability.product_difference line 113
5. theorem OAI.BoltzmannNonuniqueness.MildStability.difference line 124
6. def OAI.BoltzmannNonuniqueness.PositiveIntegral.scalePhase line 195
7. theorem OAI.BoltzmannNonuniqueness.PositiveIntegral.scalePhase_flight line 197
8. theorem OAI.BoltzmannNonuniqueness.PositiveIntegral.value_dilation line 208
9. theorem OAI.BoltzmannNonuniqueness.PositiveIntegral.mild_dilation line 242
10. theorem OAI.BoltzmannNonuniqueness.PositiveIntegral.characteristic_ae line 278
11. theorem OAI.BoltzmannNonuniqueness.PositiveIntegral.localized_characteristic line 309

    Source documentation

    The damping parameter of the iteration cancels, leaving the physical source g-L*F plus the differentiated cutoff in a unit-damped formula.

    theorem localized_characteristic {T L S : ℝ} (hT : 0 ≤ T)
        {f₀ : JetPrototype.Phase → ℝ} (hf₀ : Measurable f₀)
        {F g : ℝ × JetPrototype.Phase → ℝ} (hFm : Measurable F) (hgm : Measurable g)
        (hg : ∀ z, |g z| ≤ S)
        (hmild : ∀ t ∈ Icc 0 T, (fun p => F (t,p)) =ᵐ[FlightMeasure.phaseVolume]
          (fun p => value T L JetBarrier.flight f₀ g (t,p)))
        (χ χ' : JetPrototype.Phase → ℝ → ℝ)
        (hχ : ∀ p, ContinuousOn (χ p) (Icc 0 T))
        (hχ' : ∀ p, ContinuousOn (χ' p) (Icc 0 T))
        (hdχ : ∀ p t, t ∈ Icc 0 T → HasDerivAt (χ p) (χ' p t) t) :
        ∀ᵐ p ∂FlightMeasure.phaseVolume,
          χ p T*F (T,JetBarrier.flight T p) = Real.exp (-T)*χ p 0*f₀ p +
    …

    Mentions: OAI.BoltzmannNonuniqueness.JetPrototype.Phase, OAI.BoltzmannNonuniqueness.FlightMeasure.phaseVolume, OAI.BoltzmannNonuniqueness.PositiveIntegral.value, OAI.BoltzmannNonuniqueness.JetBarrier.flight

12. theorem OAI.BoltzmannNonuniqueness.PositiveIntegral.tested_characteristic line 362
13. theorem OAI.BoltzmannNonuniqueness.PositiveIntegral.survival_characteristic line 412
14. theorem OAI.BoltzmannNonuniqueness.PositiveIntegral.undamped_characteristic line 462
15. theorem OAI.BoltzmannNonuniqueness.PositiveIntegral.netSource_integrable_characteristic line 495