OAI/MathematicalPhysics/Boltzmann/Branching/DampedBranchingBlocks.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BoltzmannNonuniqueness.TransportPrimitive.damped line 23
2. theorem OAI.BoltzmannNonuniqueness.TransportPrimitive.damped_eq line 26
3. theorem OAI.BoltzmannNonuniqueness.TransportPrimitive.damped_continuousOn line 39
4. theorem OAI.BoltzmannNonuniqueness.TransportPrimitive.primitive_integration_by_parts line 48
5. theorem OAI.BoltzmannNonuniqueness.TransportPrimitive.damped_integration_by_parts line 65

   Source documentation

   Weak integration by parts for measurable characteristic forcing.

   theorem damped_integration_by_parts {T L c : ℝ} (hT : 0 ≤ T) {g ψ ψ' : ℝ → ℝ}
       (hg : IntervalIntegrable g volume 0 T)
       (hψ : ContinuousOn ψ (Icc 0 T)) (hψ' : ContinuousOn ψ' (Icc 0 T))
       (hdψ : ∀ t ∈ Icc 0 T, HasDerivAt ψ (ψ' t) t) :
       (∫ t in 0..T, ψ' t*damped L c g t + ψ t*(g t-L*damped L c g t)) =
         ψ T*damped L c g T - ψ 0*c := by
   …

   Mentions: OAI.BoltzmannNonuniqueness.TransportPrimitive.damped

6. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedMediumBlockMass line 136
7. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.damped_finite_history_block_transfer line 140
8. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.uniform_damped_perturbed_block_growth line 197
9. theorem OAI.BoltzmannNonuniqueness.DampedSupersolution.integral_bound line 233
10. theorem OAI.BoltzmannNonuniqueness.TransportPrimitive.survival_of_derivative_bound line 293
11. theorem OAI.BoltzmannNonuniqueness.TransportPrimitive.damped_absolutelyContinuous line 325
12. theorem OAI.BoltzmannNonuniqueness.TransportPrimitive.damped_derivative_ae line 337
13. theorem OAI.BoltzmannNonuniqueness.TransportPrimitive.damped_survival line 357
14. theorem OAI.BoltzmannNonuniqueness.Published.fourier_line_translation line 387
15. theorem OAI.BoltzmannNonuniqueness.Published.damped_phase_character line 395
16. theorem OAI.BoltzmannNonuniqueness.Published.fourier_dampedLine line 405
17. theorem OAI.BoltzmannNonuniqueness.TransportPrimitive.localized_damped line 432

    Source documentation

    A smooth cutoff of a measurable-forcing mild solution has an explicit unit-damped formula. This is the scalar part of the GLPS localization.

    theorem localized_damped {T L c : ℝ} (hT : 0 ≤ T) {g χ χ' : ℝ → ℝ}
        (hg : IntervalIntegrable g volume 0 T)
        (hχ : ContinuousOn χ (Icc 0 T)) (hχ' : ContinuousOn χ' (Icc 0 T))
        (hdχ : ∀ t ∈ Icc 0 T, HasDerivAt χ (χ' t) t) :
        χ T*damped L c g T = Real.exp (-T)*χ 0*c +
          ∫ t in 0..T, Real.exp (-(T-t)) *
            (χ t*g t + (χ' t+(1-L)*χ t)*damped L c g t) := by
    …

    Mentions: OAI.BoltzmannNonuniqueness.TransportPrimitive.damped

18. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedMediumWord_integral line 491
19. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedMediumFlightSeed line 526
20. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedMediumBlockMass_kernel line 529
21. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedBoundedEventKernel line 560
22. instance OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedBoundedEventKernel_sFinite line 564
23. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedBoundedEventKernel_lintegral line 569
24. instance OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedBoundedEventKernel_pow_sFinite line 584
25. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedBoundedWord_integral line 595
26. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedBoundedBlockIntegrand line 651
27. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedBoundedBlockMass line 658
28. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.damped_bounded_word_integrand_bound line 663
29. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.damped_bounded_word_integral_lower line 682
30. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.damped_bounded_finite_history_block_transfer line 719
31. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.uniform_damped_bounded_block_growth line 776
32. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedMediumFlightSeed_measurable line 812
33. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedBoundedEndpointKernel line 817
34. instance OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedBoundedEndpointKernel_isSFinite line 822
35. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedBoundedEndpointKernel_lintegral line 832
36. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedBoundedEndpointKernel_apply line 844
37. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedBoundedBlockMass_endpoints line 854
38. theorem OAI.BoltzmannNonuniqueness.TransportPrimitive.damped_change_rate line 884
39. theorem OAI.BoltzmannNonuniqueness.TransportPrimitive.changed_forcing_intervalIntegrable line 921