OAI/MathematicalPhysics/Boltzmann/Compactness/EntropyIntegralBalance.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BoltzmannNonuniqueness.scalarRelativeEntropy line 23
2. theorem OAI.BoltzmannNonuniqueness.scalarRelativeEntropy_eq line 25
3. theorem OAI.BoltzmannNonuniqueness.scalarRelativeEntropy_continuous line 33
4. theorem OAI.BoltzmannNonuniqueness.scalarRelativeEntropy_hasDerivAt line 36
5. def OAI.BoltzmannNonuniqueness.regularizedEntropy line 46
6. theorem OAI.BoltzmannNonuniqueness.regularizedEntropy_continuous_delta line 49
7. theorem OAI.BoltzmannNonuniqueness.regularizedEntropy_tendsto line 55
8. theorem OAI.BoltzmannNonuniqueness.regularizedEntropy_hasDerivAt line 63
9. theorem OAI.BoltzmannNonuniqueness.extendedEntropyProduction_symm line 100
10. theorem OAI.BoltzmannNonuniqueness.measurable_extendedEntropyProduction line 116
11. theorem OAI.BoltzmannNonuniqueness.production_eventually_eq line 127
12. theorem OAI.BoltzmannNonuniqueness.tendsto_extendedEntropyProduction_positive line 134
13. theorem OAI.BoltzmannNonuniqueness.tendsto_extendedEntropyProduction_zero_left line 150

    Source documentation

    A zero product against a positive product has infinite limiting production.

    theorem tendsto_extendedEntropyProduction_zero_left {ι : Type*} {l : Filter ι}
        {a b : ι → ℝ} {B : ℝ}
        (ha : Tendsto a l (𝓝 0)) (hb : Tendsto b l (𝓝 B)) (hB : 0 < B)
        (hap : ∀ᶠ i in l, 0 < a i) (hbp : ∀ᶠ i in l, 0 < b i) :
        Tendsto (fun i => extendedEntropyProduction (a i) (b i)) l (𝓝 ∞) := by
    …

    Mentions: OAI.BoltzmannNonuniqueness.extendedEntropyProduction

14. theorem OAI.BoltzmannNonuniqueness.tendsto_extendedEntropyProduction_zero_right line 168
15. theorem OAI.BoltzmannNonuniqueness.extendedEntropyProduction_le_liminf line 176
16. theorem OAI.BoltzmannNonuniqueness.lintegral_extendedEntropyProduction_le_liminf line 199

    Source documentation

    Weighted Fatou for the actual extended production, including infinite values.

    theorem lintegral_extendedEntropyProduction_le_liminf
        {X ι : Type*} [MeasurableSpace X] {μ : Measure X} {l : Filter ι}
        [NeBot l] [IsCountablyGenerated l]
        {a b : ι → X → ℝ} {A B : X → ℝ} {w : X → ℝ≥0∞}
        (ha : ∀ i, Measurable (a i)) (hb : ∀ i, Measurable (b i)) (hw : Measurable w)
        (hA : ∀ᵐ x ∂μ, 0 ≤ A x) (hB : ∀ᵐ x ∂μ, 0 ≤ B x)
        (hconv : ∀ᵐ x ∂μ, Tendsto (fun i => a i x) l (𝓝 (A x)) ∧
          Tendsto (fun i => b i x) l (𝓝 (B x)))
        (hpos : ∀ᵐ x ∂μ, (∀ᶠ i in l, 0 < a i x) ∧ (∀ᶠ i in l, 0 < b i x)) :
        (∫⁻ x, w x * extendedEntropyProduction (A x) (B x) ∂μ) ≤
          liminf (fun i => ∫⁻ x, w x * extendedEntropyProduction (a i x) (b i x) ∂μ) l := by
    …

    Mentions: OAI.BoltzmannNonuniqueness.extendedEntropyProduction

17. theorem OAI.BoltzmannNonuniqueness.extendedEntropyProduction_regularized_le_liminf line 222

    Source documentation

    Positive perturbations of four nonnegative factors provide admissible approximations.

    theorem extendedEntropyProduction_regularized_le_liminf
        {a b c d ga gb gc gd : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hc : 0 ≤ c) (hd : 0 ≤ d)
        (hga : 0 < ga) (hgb : 0 < gb) (hgc : 0 < gc) (hgd : 0 < gd) :
        extendedEntropyProduction (a * b) (c * d) ≤
          liminf (fun δ : ℝ => extendedEntropyProduction
            ((a + δ * ga) * (b + δ * gb)) ((c + δ * gc) * (d + δ * gd))) (𝓝[>] 0) := by
    …

    Mentions: OAI.BoltzmannNonuniqueness.extendedEntropyProduction

18. theorem OAI.BoltzmannNonuniqueness.scalarRelativeEntropy_nonneg line 261
19. theorem OAI.BoltzmannNonuniqueness.scalarRelativeEntropy_le_power line 266
20. theorem OAI.BoltzmannNonuniqueness.abs_log_maxwellian_le line 282
21. def OAI.BoltzmannNonuniqueness.entropyPowerMajorant line 289
22. theorem OAI.BoltzmannNonuniqueness.scalarRelativeEntropy_le_majorant line 293
23. theorem OAI.BoltzmannNonuniqueness.entropyPowerMajorant_integrable line 309
24. theorem OAI.BoltzmannNonuniqueness.bounded_relative_entropy_integrable line 320
25. theorem OAI.BoltzmannNonuniqueness.regularizedEntropy_lipschitz line 351
26. theorem OAI.BoltzmannNonuniqueness.regularizedEntropy_chain_rule line 369
27. theorem OAI.BoltzmannNonuniqueness.regularizedEntropy_integral_path line 401
28. theorem OAI.BoltzmannNonuniqueness.continuous_path_bounds_of_ae line 438
29. theorem OAI.BoltzmannNonuniqueness.regularizedEntropy_integral_path_of_ae_bounds line 453
30. def OAI.BoltzmannNonuniqueness.entropyPath line 485
31. theorem OAI.BoltzmannNonuniqueness.entropy_integral_balance line 488