Documentation

LeanPool.CaffarelliKohnNirenberg.Foundation.Parabolic.Integration.Slice

Spatial and space-time averages #

This file gives named wrappers for the two averages used on parabolic cylinders. The definitions remain the ordinary Mathlib set averages, so existing average, eLpNorm, and restriction lemmas apply without a second normalization convention.

source
noncomputable def CKN.Foundation.Parabolic.Integration.spatialAverage (x : Vec3) (r s : ℝ) (g : ParabolicPoint → ℝ) :
ℝ

The spatial average of a scalar function at a fixed time.

Equations
Instances For
    source
    noncomputable def CKN.Foundation.Parabolic.Integration.cylinderAverage (x : Vec3) (t r : ℝ) (g : ParabolicPoint → ℝ) :
    ℝ

    The space-time average of a scalar function on a parabolic cylinder.

    Equations
    Instances For
      source
      theorem CKN.Foundation.Parabolic.Integration.spatialAverage_eq_toReal_inv_smul (x : Vec3) (r s : ℝ) (g : ParabolicPoint → ℝ) :
      spatialAverage x r s g = (MeasureTheory.volume (vec3Ball x r)).toReal⁻¹ • ∫ (y : Vec3) in vec3Ball x r, g (y, s)

      The spatial average is the normalized spatial integral.

      source
      theorem CKN.Foundation.Parabolic.Integration.spatialAverage_abs_le {x : Vec3} {r s : ℝ} {g : ParabolicPoint → ℝ} :
      |spatialAverage x r s g| ≤ ⨍ (y : Vec3) in vec3Ball x r, |g (y, s)|

      The spatial average is bounded by the average of the absolute value.

      source
      theorem CKN.Foundation.Parabolic.Integration.setAverage_abs_rpow_le {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {f : α → ℝ} {p : ℝ} (hp : 1 ≤ p) (hsPos : 0 < μ s) (hsTop : μ s < ⊤) (hf : MeasureTheory.IntegrableOn (fun (x : α) => |f x|) s μ) (hfp : MeasureTheory.IntegrableOn (fun (x : α) => |f x| ^ p) s μ) :
      (⨍ (x : α) in s, |f x| ∂μ) ^ p ≤ ⨍ (x : α) in s, |f x| ^ p ∂μ

      Jensen's inequality for a nonnegative real power of a set average.

      source
      theorem CKN.Foundation.Parabolic.Integration.setAverage_norm_rpow_le {α : Type u_1} {E : Type u_2} [MeasurableSpace α] [NormedAddCommGroup E] [NormedSpace ℝ E] {μ : MeasureTheory.Measure α} {s : Set α} {f : α → E} {p : ℝ} (hp : 1 ≤ p) (hsPos : 0 < μ s) (hsTop : μ s < ⊤) (hf : MeasureTheory.IntegrableOn f s μ) (hfp : MeasureTheory.IntegrableOn (fun (x : α) => ‖f x‖ ^ p) s μ) :
      ‖⨍ (x : α) in s, f x ∂μ‖ ^ p ≤ ⨍ (x : α) in s, ‖f x‖ ^ p ∂μ

      Jensen's inequality for the norm of a vector-valued set average.

      source
      theorem CKN.Foundation.Parabolic.Integration.setLaverage_norm_sub_setAverage_rpow_le {α : Type u_1} {E : Type u_2} [MeasurableSpace α] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {μ : MeasureTheory.Measure α} {s : Set α} {f : α → E} {p : ℝ} {c : E} (hp : 1 ≤ p) (hsPos : 0 < μ s) (hsTop : μ s < ⊤) (hf : MeasureTheory.IntegrableOn f s μ) (hfp : MeasureTheory.IntegrableOn (fun (x : α) => ‖f x - c‖ ^ p) s μ) :
      ⨍⁻ (x : α) in s, ‖f x - ⨍ (y : α) in s, f y ∂μ‖ₑ ^ p ∂μ ≤ 2 ^ p * ⨍⁻ (x : α) in s, ‖f x - c‖ₑ ^ p ∂μ

      Mean oscillation is bounded by 2^p times the oscillation around any constant.

      source
      theorem CKN.Foundation.Parabolic.Integration.setLaverage_abs_sub_setAverage_rpow_le {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {f : α → ℝ} {p c : ℝ} (hp : 1 ≤ p) (hsPos : 0 < μ s) (hsTop : μ s < ⊤) (hf : MeasureTheory.IntegrableOn f s μ) (hfp : MeasureTheory.IntegrableOn (fun (x : α) => |f x - c| ^ p) s μ) :
      ⨍⁻ (x : α) in s, ‖f x - ⨍ (y : α) in s, f y ∂μ‖ₑ ^ p ∂μ ≤ 2 ^ p * ⨍⁻ (x : α) in s, ‖f x - c‖ₑ ^ p ∂μ

      Scalar mean oscillation is bounded by 2^p times oscillation around a constant.

      source
      theorem CKN.Foundation.Parabolic.Integration.ball_setLaverage_abs_sub_spatialAverage_rpow_le {x : Vec3} {r s : ℝ} {g : ParabolicPoint → ℝ} {p c : ℝ} (hp : 1 ≤ p) (hr : 0 < r) (hg : MeasureTheory.IntegrableOn (fun (y : Vec3) => g (y, s)) (vec3Ball x r) MeasureTheory.volume) (hgp : MeasureTheory.IntegrableOn (fun (y : Vec3) => |g (y, s) - c| ^ p) (vec3Ball x r) MeasureTheory.volume) :
      ⨍⁻ (y : Vec3) in vec3Ball x r, ‖g (y, s) - spatialAverage x r s g‖ₑ ^ p ∂MeasureTheory.volume ≤ 2 ^ p * ⨍⁻ (y : Vec3) in vec3Ball x r, ‖g (y, s) - c‖ₑ ^ p ∂MeasureTheory.volume

      Scalar mean oscillation on a positive-radius spatial ball.

      source
      theorem CKN.Foundation.Parabolic.Integration.setAverage_abs_rpow_norm_mono {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {f : α → ℝ} {p q : ℝ} (hq1 : 1 ≤ q) (hqp : q ≤ p) (hsPos : 0 < μ s) (hsTop : μ s < ⊤) (hf : MeasureTheory.IntegrableOn f s μ) (hp : MeasureTheory.IntegrableOn (fun (x : α) => |f x| ^ p) s μ) :
      (⨍ (x : α) in s, |f x| ^ q ∂μ) ^ q⁻¹ ≤ (⨍ (x : α) in s, |f x| ^ p ∂μ) ^ p⁻¹

      Normalized scalar Hölder monotonicity on a finite positive-measure set.

      source
      theorem CKN.Foundation.Parabolic.Integration.setAverage_abs_le_rpow_mean {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {f : α → ℝ} {p : ℝ} (hp : 1 ≤ p) (hsPos : 0 < μ s) (hsTop : μ s < ⊤) (hf : MeasureTheory.IntegrableOn f s μ) (hfp : MeasureTheory.IntegrableOn (fun (x : α) => |f x| ^ p) s μ) :
      |⨍ (x : α) in s, f x ∂μ| ≤ (⨍ (x : α) in s, |f x| ^ p ∂μ) ^ p⁻¹

      The absolute value of a set average is bounded by the normalized Lᵖ mean.

      source
      theorem CKN.Foundation.Parabolic.Integration.ball_lintegral_norm_sq_mono_radius {x : Vec3} {r₁ r₂ s : ℝ} (hrr : r₁ ≤ r₂) (g : ParabolicPoint → ℝ) :
      ∫⁻ (y : Vec3) in vec3Ball x r₁, ‖g (y, s)‖ₑ ^ 2 ≤ ∫⁻ (y : Vec3) in vec3Ball x r₂, ‖g (y, s)‖ₑ ^ 2

      The spatial L² lintegral is monotone with the ball radius.