OAI/MathematicalPhysics/Boltzmann/Jets/CoreDensityTranslation.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BoltzmannNonuniqueness.JetCoreDensity.thermalCoordinates line 22
2. def OAI.BoltzmannNonuniqueness.JetCoreDensity.thermalWeight line 25
3. def OAI.BoltzmannNonuniqueness.JetCoreDensity.thermalPoint line 28
4. theorem OAI.BoltzmannNonuniqueness.JetCoreDensity.thermalCoordinates_measurePreserving line 32
5. theorem OAI.BoltzmannNonuniqueness.JetCoreDensity.thermalWeight_measurable line 37
6. theorem OAI.BoltzmannNonuniqueness.JetCoreDensity.thermalPoint_measurable line 42
7. theorem OAI.BoltzmannNonuniqueness.JetCoreDensity.core_thermal_integral line 48
8. theorem OAI.BoltzmannNonuniqueness.JetCoreDensity.thermalCoordinates_apply line 65
9. theorem OAI.BoltzmannNonuniqueness.JetCoreDensity.thermalPoint_eq_center line 71
10. theorem OAI.BoltzmannNonuniqueness.JetCoreDensity.thermalWeight_bound line 103
11. theorem OAI.BoltzmannNonuniqueness.JetCoreDensity.thermalWeight_zero line 112
12. theorem OAI.BoltzmannNonuniqueness.JetCoreDensity.dilated_thermalWeight_bound line 120
13. abbrev OAI.BoltzmannNonuniqueness.JetCoreDensity.ThermalArguments line 154
14. theorem OAI.BoltzmannNonuniqueness.JetCoreDensity.clamped_sourceFoot_measurable line 156
15. theorem OAI.BoltzmannNonuniqueness.JetCoreDensity.clamped_axialMap_measurable line 165
16. theorem OAI.BoltzmannNonuniqueness.JetCoreDensity.clamped_thermalPoint_measurable line 177
17. theorem OAI.BoltzmannNonuniqueness.JetCoreDensity.clamped_thermalWeight_measurable line 191
18. def OAI.BoltzmannNonuniqueness.JetCoreSheet.slabAmplitude line 245
19. theorem OAI.BoltzmannNonuniqueness.JetCoreSheet.slabAmplitude_nonneg line 248
20. theorem OAI.BoltzmannNonuniqueness.JetCoreSheet.amplitude_le_slab line 254
21. theorem OAI.BoltzmannNonuniqueness.JetCoreSheet.core_bands_small_of_card line 268

    Source documentation

    The radius is uniform in the interval centers, core scale, and thermal width.

    theorem core_bands_small_of_card {K α γ q a ε : ℝ} (hK : 0 ≤ K)
        (hα : 0 < α) (hγ : 0 < γ) (hq₁ : 1 < q) (hq₂ : q < 2)
        (ha : 0 < a) (hε : 0 < ε) (N : ℕ) :
        ∃ δ : ℝ, 0 < δ ∧ ∀ {s d t : ℝ}, 0 < s → 0 < d → d ≤ 1/16 → a ≤ t →
          ∀ (η : ℝ) (sign : Bool) (x : JetPrototype.Space) (v : Velocity) (S : Finset ℝ),
          S.card ≤ N →
          ChartKernel.offAxis (normalizedCoreKernel η K α γ s d q sign) ((t,x),v)
            (axial ⁻¹' bands S δ) ≤ ENNReal.ofReal ε := by
    …

    Mentions: OAI.BoltzmannNonuniqueness.JetPrototype.Space, OAI.BoltzmannNonuniqueness.Velocity, OAI.BoltzmannNonuniqueness.ChartKernel.offAxis, OAI.BoltzmannNonuniqueness.JetCoreSheet.normalizedCoreKernel

22. theorem OAI.BoltzmannNonuniqueness.JetCoreSheet.core_away_small_of_transverse line 325
23. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.spatialMap_dilated_translate line 373
24. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.copyCoreDensity_eq line 379