The γ-form Caccioppoli terms #
paper/ckn.tex, Lemma lem:caccioppoli-gamma (eq:caccioppoli-gamma), reruns
the proof of the Caccioppoli inequality lem:caccioppoli changing only the
bounds on the first two of the four error terms. This file records those two
replacement bounds as standalone theorems about the same raw integrals that
CKN.Core.Caccioppoli.RawI1 and CKN.Core.Caccioppoli.RawI2Bound bound.
I₁: the test-function weight|∂ₛφ + Δφ|is bounded pointwise byC r² ρ⁻⁵, and∫∫_{Q_ρ}|u|²is estimated by Hölder with1 = 2/3 + 1/3,∫∫_{Q_ρ}|u|² ≤ |Q_ρ|^{1/3} (∫∫_{Q_ρ}|u|³)^{2/3} = C ρ³ γ(ρ)². HenceI₁ ≤ C κ² γ(ρ)²withκ = r/ρ(caccioppoli_I1_gamma_heat_cutoff_raw_bound).I₂: the Poincaré input is dropped; instead||u|² − ⨍_{B_ρ}|u|²| |u| ≤ 2|u|³ + (⨍_{B_ρ}|u|²)^{3/2}pointwise, the spatial average enters through the Jensen bound⨍_{B_ρ}|u|² ≤ (⨍_{B_ρ}|u|³)^{2/3}, and∫∫_{Q_ρ}|u|³ = ρ² γ(ρ)³givesI₂ ≤ C κ⁻² γ(ρ)³(caccioppoli_I2_gamma_heat_cutoff_raw_bound).
The remaining two terms I₃, I₄ keep their proved bounds, so the conclusion
of eq:caccioppoli-gamma follows by the normalisation lemmas recorded here.
The two elementary estimates behind the replacement bounds #
Hölder's inequality on a measure space with conjugate exponents 3/2 and 3
in the form used for I₁: the integral of a nonnegative function is bounded by
(∫ A^{3/2})^{2/3} times the 1/3 power of the total mass.
The pointwise inequality behind I₂ in its γ-form: for N, m ≥ 0,
|N² − m| N ≤ 2 N³ + m^{3/2}. This combines the triangle inequality for the
mean subtraction with the Young inequality mN ≤ m^{3/2} + N³.
The ℝ≥0∞ form of caccioppoli_abs_sq_sub_mul_le, ready for integration.
The two N³ terms are kept separate so that each can be matched against the
velocity integral ∫∫_{Q_ρ}|u|³, and the exponent 3 of N is the real one so
that the term is literally (ENNReal.ofReal N) ^ (3 : ℝ), the integrand of the
velocity identity caccioppoli_I2_velocity_integral_identity.
The L² estimate for the velocity in the γ-form Caccioppoli inequality:
Hölder's inequality on Q_ρ with 1 = 2/3 + 1/3 combined with
∫∫_{Q_ρ}|u|³ = ρ² γ(ρ)³ gives
∫∫_{Q_ρ}|u|² ≤ |Q_ρ|^{1/3} (∫∫_{Q_ρ}|u|³)^{2/3} = (4π/3)^{1/3} ρ³ γ(ρ)².
The I₁ replacement bound #
The I₁ replacement bound of Lemma lem:caccioppoli-gamma. Combining
the pointwise bound on the heat-cut-off weight with Hölder's inequality
1 = 2/3 + 1/3 on Q_ρ and the γ-form velocity bound
∫∫_{Q_ρ}|u|² ≤ (4π/3)^{1/3} ρ³ γ(ρ)², the first error term satisfies
I₁ ≤ C r²ρ⁻⁵ ρ³γ(ρ)² = C κ²γ(ρ)² with κ = r/ρ, the constant being the same
one that appears in the established I₁ bound times (4π/3)^{1/3}.
Normalized I₁. Reading the I₁ replacement bound as
I₁ ≤ K (r²/ρ⁵) ρ³γ(ρ)² with K = (4π/3)^{1/3}((32 + 3C'')8·10⁶ + 6C'5·10⁶)
and assuming K ≤ C₂₅², the first two terms of eq:caccioppoli-gamma give
I₁ ≤ (C₂₅ κ γ(ρ))² with κ = r/ρ.
The I₂ replacement bound #
The I₂ replacement bound of Lemma lem:caccioppoli-gamma. Here the
Poincaré input used by the established I₂ bound is replaced by the pointwise bound
||u|² − c| |u| ≤ 2|u|³ + c^{3/2} together with the Jensen bound hmean on the
spatial average c (in the application c is ⨍_{B_ρ}|u|²). Since
∫∫_{Q_ρ}|u|³ = ρ²γ(ρ)³ and the cut-off gradient contributes a factor r⁻²,
this gives I₂ ≤ C r⁻²ρ²γ(ρ)³ = C κ⁻²γ(ρ)³ with κ = r/ρ, matching the
displayed bound in the proof of Lemma lem:caccioppoli-gamma.