Conversions

Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.

theorem CKN.alpha_sq_eq (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (z : Foundation.Parabolic.ParabolicPoint) (r : ℝ) (hr : 0 < r) : alpha u z r ^ 2 = r⁻¹ * (Foundation.Parabolic.Integration.timeSliceEnergyEssSup z.1 z.2 r fun (w : Foundation.Parabolic.ParabolicPoint) => Foundation.Parabolic.vec3EuclideanNorm (u w)).toReal

The square of alpha is its normalized time-slice energy.

theorem CKN.beta_sq_eq (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3) (z : Foundation.Parabolic.ParabolicPoint) (r : ℝ) (hr : 0 < r) : beta u Du z r ^ 2 = r⁻¹ * (∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder z.1 z.2 r, ENNReal.ofReal (spatialGradientSq u Du w)).toReal

The square of beta is its normalized gradient integral.

theorem CKN.gamma_cube_eq (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (z : Foundation.Parabolic.ParabolicPoint) (r : ℝ) (hr : 0 < r) : gamma u z r ^ 3 = r ^ (-2) * (∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder z.1 z.2 r, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u w)) ^ 3).toReal

The cube of gamma is its normalized velocity integral.

theorem CKN.delta_cube_eq (p : Foundation.Parabolic.ParabolicPoint → ℝ) (z : Foundation.Parabolic.ParabolicPoint) (r : ℝ) (hr : 0 < r) : delta p z r ^ 3 = r ^ (-2) * (∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder z.1 z.2 r, ENNReal.ofReal |p w| ^ (3 / 2)).toReal

The cube of delta is its normalized pressure integral.

theorem CKN.lambda_pow_eq (q : ℝ) (f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (z : Foundation.Parabolic.ParabolicPoint) (r : ℝ) (hr : 0 < r) (hq : 0 < q) : lambda q f z r ^ q = (r ^ (3 - 5 / q)) ^ q * (∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder z.1 z.2 r, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (f w)) ^ q).toReal

The q-power of lambda separates its radius factor and force integral.

theorem CKN.setIntegral_eq_toReal_setLIntegral_of_nonneg {α : Type u_1} [MeasureTheory.MeasureSpace α] {s : Set α} {g : α → ℝ} (hg : MeasureTheory.IntegrableOn g s MeasureTheory.volume) (hgn : 0 ≤ᵐ[MeasureTheory.volume.restrict s] g) : ∫ (x : α) in s, g x = (∫⁻ (x : α) in s, ENNReal.ofReal (g x)).toReal

A nonnegative Bochner set integral is the real form of its ofReal lintegral.