CarlemanOperator.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Nonnegative Carleman gain

Gamba, Panferov and Villani, Upper Maxwellian bounds for the spatially homogeneous Boltzmann equation, Arch. Ration. Mech. Anal. 194 (2009), 253–282, Appendix C, Lemma 16 and the hard-sphere remark. The author's preprint https://www.csun.edu/~panferov/research/umb_5.pdf gives the formula on pp. 23–24. Their hard-sphere rate is |g|/(4π) in outgoing-direction coordinates. Multiplication by 2π gives the present absolute-normal kernel and the coefficient 2 below.

The nonnegative measurable form of that identity is expressed in an explicit plane chart. Its density formulation includes the plane-chart measure identification and allows arbitrary nonnegative measurable densities.

def OAI.BoltzmannNonuniqueness.nonnegativeGain line 32
Source documentation
The nonnegative symmetric gain in the original normal-sphere variables.
```
def nonnegativeGain (f g : Velocity → ℝ≥0∞) (v : Velocity) : ℝ≥0∞ :=
…
```
Mentions: OAI.BoltzmannNonuniqueness.Velocity
def OAI.BoltzmannNonuniqueness.chartGain line 40
Source documentation
Carleman gain against a possibly singular incoming velocity measure. The transverse degeneracy set has measure zero for the sheet laws used here.
```
def chartGain (c : Measure Velocity) (h : Velocity → ℝ≥0∞) (v : Velocity) : ℝ≥0∞ :=
…
```
Mentions: OAI.BoltzmannNonuniqueness.Velocity
def OAI.BoltzmannNonuniqueness.chartRegionGain line 46
Source documentation
Restriction in the actual incoming velocity and the two chart coordinates.
```
def chartRegionGain (c : Measure Velocity) (h : Velocity → ℝ≥0∞) (v : Velocity)
    (S : Set (Velocity × (ℝ × ℝ))) : ℝ≥0∞ := by
…
```
Mentions: OAI.BoltzmannNonuniqueness.Velocity
def OAI.BoltzmannNonuniqueness.normalizedChartGain line 53
def OAI.BoltzmannNonuniqueness.normalizedChartRegionGain line 56
theorem OAI.BoltzmannNonuniqueness.chart_weight_ratio_le line 61
Source documentation
The algebraic estimate applies to every nondegenerate point of the actual chart.
```
theorem chart_weight_ratio_le (q : ℝ) (v p : Velocity) (z s : ℝ)
    (hn : normal v p ≠ 0) :
    VelocityWeight.H q (chart v p z s) / VelocityWeight.H q v ≤
      VelocityWeight.tiltConstant *
        Real.exp (2 * ‖p‖ ^ 2 - ‖companionVelocity p (chart v p z s) v‖ ^ 2) *
        (VelocityWeight.W q (chart v p z s) / VelocityWeight.W q v) :=
…
```
Mentions: OAI.BoltzmannNonuniqueness.Velocity, OAI.BoltzmannNonuniqueness.VelocityWeight.H, OAI.BoltzmannNonuniqueness.VelocityWeight.tiltConstant, OAI.BoltzmannNonuniqueness.companionVelocity, OAI.BoltzmannNonuniqueness.VelocityWeight.W
def OAI.BoltzmannNonuniqueness.Published.GPV2009CarlemanInput line 74
Source documentation
The application-specific nonnegative form of the published Carleman identity. For densities the zero transverse-normal set is Lebesgue null. The statement does not assert equality for arbitrary singular incoming measures.
```
def GPV2009CarlemanInput : Prop :=
…
```
theorem OAI.BoltzmannNonuniqueness.chartGain_mono_right line 81
theorem OAI.BoltzmannNonuniqueness.chartGain_mono_measure line 87
theorem OAI.BoltzmannNonuniqueness.chartGain_add_measure line 93
theorem OAI.BoltzmannNonuniqueness.chartGain_smul_measure line 98
theorem OAI.BoltzmannNonuniqueness.nonnegativeGain_le_of_chartGain line 108
Source documentation
A bound proved for the explicit chart gain transfers to the original gain under the stated published input.
```
theorem nonnegativeGain_le_of_chartGain
    (hcarleman : Published.GPV2009CarlemanInput)
    {f g : Velocity → ℝ≥0∞} (hf : Measurable f) (hg : Measurable g)
    {B : Velocity → ℝ≥0∞}
    (hB : ∀ᵐ v : Velocity ∂volume, chartGain (volume.withDensity f) g v ≤ B v) :
    ∀ᵐ v : Velocity ∂volume, nonnegativeGain f g v ≤ B v := by
…
```
Mentions: OAI.BoltzmannNonuniqueness.Published.GPV2009CarlemanInput, OAI.BoltzmannNonuniqueness.Velocity, OAI.BoltzmannNonuniqueness.chartGain, OAI.BoltzmannNonuniqueness.nonnegativeGain