PowerDiskMixture.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

The positive disk mixture for the truncated transverse power

The hot-gain estimate uses the finite measure with density (1 + ‖p‖⁻ᑫ) 1_{‖p‖ < D}. Its singular part is a positive radius mixture of centered disks. Values at the origin are irrelevant for this identity.

def OAI.BoltzmannNonuniqueness.PowerDiskMixture.mixingDensity line 22
def OAI.BoltzmannNonuniqueness.PowerDiskMixture.cutoffDensity line 24
theorem OAI.BoltzmannNonuniqueness.PowerDiskMixture.integral_power_tail line 27
theorem OAI.BoltzmannNonuniqueness.PowerDiskMixture.mixingDensity_nonneg line 39
theorem OAI.BoltzmannNonuniqueness.PowerDiskMixture.measurable_mixingDensity line 44
theorem OAI.BoltzmannNonuniqueness.PowerDiskMixture.integrableOn_mixingDensity line 48
theorem OAI.BoltzmannNonuniqueness.PowerDiskMixture.integral_mixingDensity line 54
theorem OAI.BoltzmannNonuniqueness.PowerDiskMixture.layerCake_integrand line 63
theorem OAI.BoltzmannNonuniqueness.PowerDiskMixture.density_layerCake line 79
Source documentation
The singular radial density is a positive mixture of disks, away from its null origin.
```
theorem density_layerCake {q D : ℝ} (hq : 0 < q) (_hD : 0 < D)
    {p : Transverse} (hp : p ≠ 0) :
    cutoffDensity q D p =
      (1 + D ^ (-q)) * (ball (0 : Transverse) D).indicator (fun _ => 1) p +
        ∫ a in Ioc 0 D, mixingDensity q a * diskDensity a p := by
…
```
Mentions: OAI.BoltzmannNonuniqueness.PowerDiskMixture.cutoffDensity, OAI.BoltzmannNonuniqueness.PowerDiskMixture.mixingDensity
theorem OAI.BoltzmannNonuniqueness.PowerDiskMixture.layerCake_indicator line 109
theorem OAI.BoltzmannNonuniqueness.PowerDiskMixture.integrableOn_layerCake line 124
def OAI.BoltzmannNonuniqueness.PowerDiskMixture.boundaryMass line 135
theorem OAI.BoltzmannNonuniqueness.PowerDiskMixture.boundaryMass_nonneg line 137
theorem OAI.BoltzmannNonuniqueness.PowerDiskMixture.lintegral_density_layerCake line 142
theorem OAI.BoltzmannNonuniqueness.PowerDiskMixture.measurable_diskDensity_fixed line 165

theorem OAI.BoltzmannNonuniqueness.PowerDiskMixture.lintegral_cutoff_mixture line 171

Source documentation

Tonelli's theorem turns the density identity into a positive mixture for every nonnegative measurable test, including singular kernel tests.

theorem lintegral_cutoff_mixture {q D : ℝ} (hq : 0 < q) (hD : 0 < D)
    (φ : Transverse → ℝ≥0∞) (hφ : Measurable φ) :
    (∫⁻ p, ENNReal.ofReal (cutoffDensity q D p) * φ p) =
      ENNReal.ofReal (boundaryMass q D) *
        (∫⁻ p, ENNReal.ofReal (diskDensity D p) * φ p) +
      ∫⁻ a in Ioc 0 D, ENNReal.ofReal (mixingDensity q a) *
        (∫⁻ p, ENNReal.ofReal (diskDensity a p) * φ p) := by
…

Mentions: OAI.BoltzmannNonuniqueness.PowerDiskMixture.cutoffDensity, OAI.BoltzmannNonuniqueness.PowerDiskMixture.boundaryMass, OAI.BoltzmannNonuniqueness.PowerDiskMixture.mixingDensity