OAI/MathematicalPhysics/Boltzmann/Jets/FreeCoreMismatch.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.BoltzmannNonuniqueness.JetCoreSheet.core_region_bound line 23
2. theorem OAI.BoltzmannNonuniqueness.JetCoreSheet.inputKernel_region line 38
3. theorem OAI.BoltzmannNonuniqueness.JetCoreSheet.core_tail_bound line 47
4. def OAI.BoltzmannNonuniqueness.JetCoreSheet.growthConstant line 78
5. theorem OAI.BoltzmannNonuniqueness.JetCoreSheet.growthConstant_nonneg line 82
6. theorem OAI.BoltzmannNonuniqueness.JetCoreSheet.normalizedCoreKernel_time_bound line 88
7. theorem OAI.BoltzmannNonuniqueness.JetCoreSheet.offAxisCoreKernel_time_bound line 116
8. theorem OAI.BoltzmannNonuniqueness.JetCoreSheet.core_large_output line 146
9. theorem OAI.BoltzmannNonuniqueness.JetCoreSheet.core_axis_input line 164
10. theorem OAI.BoltzmannNonuniqueness.JetCoreSheet.core_axis_mismatch line 182
11. theorem OAI.BoltzmannNonuniqueness.JetCoreSheet.core_axial_interval line 219
12. theorem OAI.BoltzmannNonuniqueness.JetCoreSheet.core_small_input line 238
13. def OAI.BoltzmannNonuniqueness.JetCoreSheet.kineticColdKernel line 276
14. instance OAI.BoltzmannNonuniqueness.JetCoreSheet.kineticColdKernel_sFinite line 281
15. def OAI.BoltzmannNonuniqueness.JetCoreSheet.kineticFreeKernel line 286
16. instance OAI.BoltzmannNonuniqueness.JetCoreSheet.kineticFreeKernel_sFinite line 289
17. theorem OAI.BoltzmannNonuniqueness.JetCoreSheet.kineticColdKernel_apply line 294
18. theorem OAI.BoltzmannNonuniqueness.JetCoreSheet.input_kineticColdKernel line 301
19. theorem OAI.BoltzmannNonuniqueness.JetCoreSheet.kineticFreeKernel_bound line 309
20. theorem OAI.BoltzmannNonuniqueness.JetCoreSheet.iterate_kineticFreeKernel_bound line 321
21. theorem OAI.BoltzmannNonuniqueness.JetFreeTransport.free_axial_speed_error line 349
22. def OAI.BoltzmannNonuniqueness.JetCoreSheet.kineticCoreDensity line 392
23. theorem OAI.BoltzmannNonuniqueness.JetCoreSheet.kineticCoreDensity_measurable line 396
24. theorem OAI.BoltzmannNonuniqueness.JetCoreSheet.iterate_kineticFree_congr_ae_at line 409
25. theorem OAI.BoltzmannNonuniqueness.JetCoreSheet.core_restrict_mismatch line 440
26. theorem OAI.BoltzmannNonuniqueness.JetCoreSheet.core_total_eq_mismatch line 464
27. theorem OAI.BoltzmannNonuniqueness.JetCoreSheet.core_mass_small_of_speed_gap line 480

    Source documentation

    The near-axis estimate controls the whole core kernel, provided its implicit cold speed stays farther away than the thermal width.

    theorem core_mass_small_of_speed_gap {α q δ ε : ℝ}
        (hq₁ : 1 < q) (hq₂ : q < 2) (hδ : 0 < δ) (hε : 0 < ε) :
        ∃ r : ℝ, 0 < r ∧ ∀ {K γ s d t : ℝ}, 0 ≤ K → 0 < α → 0 < γ →
          0 < s → 0 < d → d ≤ 1/16 → 0 ≤ t → ∀ (η : ℝ) (a : Bool)
          (x : JetPrototype.Space) (v : Velocity), transverse v ≠ 0 → ‖transverse v‖ ≤ r →
          δ+d ≤ |axial v-velocity (JetPrototype.sign a) α γ s t x.2| →
          normalizedCoreKernel η K α γ s d q a ((t,x),v) univ ≤
            ENNReal.ofReal (amplitude K α γ s t)*ENNReal.ofReal ε := by
    …

    Mentions: OAI.BoltzmannNonuniqueness.JetPrototype.Space, OAI.BoltzmannNonuniqueness.Velocity, OAI.BoltzmannNonuniqueness.JetPrototype.sign, OAI.BoltzmannNonuniqueness.JetCoreSheet.normalizedCoreKernel, OAI.BoltzmannNonuniqueness.JetCoreSheet.amplitude