Coarse-graining support: Support.Deterministic.ConstantCoefficientDirichletBesov.OverlapLp

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

noncomputable def HCPolySupport.overlapCubeAverage {d : ℕ} (S : TriadicCube d) (f : Vec d → ℝ) : ℝ

Average of a scalar field on an overlapping cube.

Equations

• HCPolySupport.overlapCubeAverage S f = (HCPolySupport.overlapCubeVolume S)⁻¹ * ∫ (x : HCPolySupport.Vec d) in HCPolySupport.overlapCubeSet S, f x

theorem HCPolySupport.overlapCubeAverage_eq_integralAverage_openOverlapCubeSet {d : ℕ} (S : TriadicCube d) (f : Vec d → ℝ) : overlapCubeAverage S f = integralAverage (openOverlapCubeSet S) f

theorem HCPolySupport.H1Function.toMeanZero_openOverlapCubeSet_apply {d : ℕ} (S : TriadicCube d) (u : H1Function (openOverlapCubeSet S)) (x : Vec d) : u.toMeanZero.toH1Function.toFun x = u.toFun x - overlapCubeAverage S fun (y : Vec d) => u.toFun y

theorem HCPolySupport.H1Function.toMeanZero_openOverlapCubeSet_grad {d : ℕ} (S : TriadicCube d) (u : H1Function (openOverlapCubeSet S)) (x : Vec d) : u.toMeanZero.toH1Function.grad x = u.grad x

noncomputable def HCPolySupport.overlapCubeAverageVec {d : ℕ} (S : TriadicCube d) (u : Vec d → Vec d) : Vec d

Coordinatewise average of a vector field on an overlapping cube.

Equations

• HCPolySupport.overlapCubeAverageVec S u i = HCPolySupport.overlapCubeAverage S fun (x : HCPolySupport.Vec d) => u x i

noncomputable def HCPolySupport.overlapCubeLpNorm {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] (S : TriadicCube d) (p : ENNReal) (u : Vec d → E) : ℝ

Normalized Lᵖ norm on an overlapping cube.

Equations

• HCPolySupport.overlapCubeLpNorm S p u = (MeasureTheory.eLpNorm u p (HCPolySupport.normalizedOverlapCubeMeasure S)).toReal

theorem HCPolySupport.overlapCubeAverage_eq_integral_normalizedOverlapCubeMeasure {d : ℕ} (S : TriadicCube d) (f : Vec d → ℝ) : overlapCubeAverage S f = ∫ (x : Vec d), f x ∂normalizedOverlapCubeMeasure S

theorem HCPolySupport.overlapCubeAverage_congr_on_overlapCubeSet {d : ℕ} {S : TriadicCube d} {u v : Vec d → ℝ} (h : ∀ x ∈ overlapCubeSet S, u x = v x) : overlapCubeAverage S u = overlapCubeAverage S v

theorem HCPolySupport.overlapCubeAverageVec_congr_on_overlapCubeSet {d : ℕ} {S : TriadicCube d} {u v : Vec d → Vec d} (h : ∀ x ∈ overlapCubeSet S, u x = v x) : overlapCubeAverageVec S u = overlapCubeAverageVec S v

theorem HCPolySupport.overlapCubeLpNorm_congr_on_overlapCubeSet_generic {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] (S : TriadicCube d) (p : ENNReal) {u v : Vec d → E} (h : ∀ x ∈ overlapCubeSet S, u x = v x) : overlapCubeLpNorm S p u = overlapCubeLpNorm S p v

@[simp]

theorem HCPolySupport.overlapCubeAverage_const {d : ℕ} (S : TriadicCube d) (c : ℝ) : (overlapCubeAverage S fun (x : Vec d) => c) = c

@[simp]

theorem HCPolySupport.overlapCubeAverageVec_const {d : ℕ} (S : TriadicCube d) (c : Vec d) : (overlapCubeAverageVec S fun (x : Vec d) => c) = c

theorem HCPolySupport.overlapCubeLpNorm_nonneg {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] (S : TriadicCube d) (p : ENNReal) (f : Vec d → E) : 0 ≤ overlapCubeLpNorm S p f

theorem HCPolySupport.overlapCubeLpNorm_const {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] (S : TriadicCube d) (p : ENNReal) (c : E) (hp : p ≠ 0) : (overlapCubeLpNorm S p fun (x : Vec d) => c) = ‖c‖

theorem HCPolySupport.overlapCubeLpNorm_one_eq_integral_norm {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] (S : TriadicCube d) (f : Vec d → E) (hf : MeasureTheory.AEStronglyMeasurable f (normalizedOverlapCubeMeasure S)) : overlapCubeLpNorm S 1 f = ∫ (x : Vec d), ‖f x‖ ∂normalizedOverlapCubeMeasure S

theorem HCPolySupport.overlapCubeLpNorm_mul_le_mul_overlapCubeLpNorm_of_holderConjugate {d : ℕ} (S : TriadicCube d) (p q : ENNReal) (f g : Vec d → ℝ) [p.HolderConjugate q] (hf : MeasureTheory.MemLp f p (normalizedOverlapCubeMeasure S)) (hg : MeasureTheory.MemLp g q (normalizedOverlapCubeMeasure S)) : (overlapCubeLpNorm S 1 fun (x : Vec d) => f x * g x) ≤ overlapCubeLpNorm S p f * overlapCubeLpNorm S q g

theorem HCPolySupport.abs_overlapCubeAverage_mul_le_mul_overlapCubeLpNorm_of_holderConjugate {d : ℕ} (S : TriadicCube d) (p q : ENNReal) (f g : Vec d → ℝ) [p.HolderConjugate q] (hf : MeasureTheory.MemLp f p (normalizedOverlapCubeMeasure S)) (hg : MeasureTheory.MemLp g q (normalizedOverlapCubeMeasure S)) : |overlapCubeAverage S fun (x : Vec d) => f x * g x| ≤ overlapCubeLpNorm S p f * overlapCubeLpNorm S q g

theorem HCPolySupport.abs_overlapCubeAverage_mul_le_mul_overlapCubeLpNorm_conjExponent {d : ℕ} (S : TriadicCube d) (p : ENNReal) (f g : Vec d → ℝ) (hf : MeasureTheory.MemLp f p (normalizedOverlapCubeMeasure S)) (hg : MeasureTheory.MemLp g p.conjExponent (normalizedOverlapCubeMeasure S)) (hp : 1 ≤ p) : |overlapCubeAverage S fun (x : Vec d) => f x * g x| ≤ overlapCubeLpNorm S p f * overlapCubeLpNorm S p.conjExponent g

theorem HCPolySupport.overlapCubeLpNorm_component_le_overlapCubeLpNorm {d : ℕ} (S : TriadicCube d) (p : ENNReal) (u : Vec d → Vec d) (i : Fin d) (hu : MeasureTheory.MemLp u p (normalizedOverlapCubeMeasure S)) : (overlapCubeLpNorm S p fun (x : Vec d) => u x i) ≤ overlapCubeLpNorm S p u

theorem HCPolySupport.norm_overlapCubeAverageVec_le_overlapCubeLpNorm_two {d : ℕ} (S : TriadicCube d) (u : Vec d → Vec d) (hu : MeasureTheory.MemLp u 2 (normalizedOverlapCubeMeasure S)) : ‖overlapCubeAverageVec S u‖ ≤ overlapCubeLpNorm S 2 u

theorem HCPolySupport.overlapCubeLpNorm_add_le {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] (S : TriadicCube d) (p : ENNReal) (f g : Vec d → E) (hf : MeasureTheory.MemLp f p (normalizedOverlapCubeMeasure S)) (hg : MeasureTheory.MemLp g p (normalizedOverlapCubeMeasure S)) (hp : 1 ≤ p) : (overlapCubeLpNorm S p fun (x : Vec d) => f x + g x) ≤ overlapCubeLpNorm S p f + overlapCubeLpNorm S p g

theorem HCPolySupport.overlapCubeLpNorm_two_vec_le_sum_components {d : ℕ} (S : TriadicCube d) (u : Vec d → Vec d) (hu : MeasureTheory.MemLp u 2 (normalizedOverlapCubeMeasure S)) : overlapCubeLpNorm S 2 u ≤ ∑ i : Fin d, overlapCubeLpNorm S 2 fun (x : Vec d) => u x i

theorem HCPolySupport.cubeLpNorm_two_sq_eq_lintegral_rpow_enorm_toReal {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] (Q : TriadicCube d) (f : Vec d → E) (hf : MeasureTheory.AEStronglyMeasurable f (normalizedCubeMeasure Q)) : cubeLpNorm Q 2 f ^ 2 = (∫⁻ (x : Vec d), ‖f x‖ₑ ^ 2 ∂normalizedCubeMeasure Q).toReal

theorem HCPolySupport.cubeLpNorm_two_sq_eq_lintegral_ofReal_sq_toReal {d : ℕ} (Q : TriadicCube d) (f : Vec d → ℝ) (hf : MeasureTheory.AEStronglyMeasurable f (normalizedCubeMeasure Q)) : cubeLpNorm Q 2 f ^ 2 = (∫⁻ (x : Vec d), ENNReal.ofReal (f x ^ 2) ∂normalizedCubeMeasure Q).toReal

theorem HCPolySupport.cubeLpNorm_two_sq_le_lintegral_ofReal_vecNormSq_toReal_of_le {d : ℕ} {Q : TriadicCube d} {F : Vec d → Vec d} {B : ENNReal} (hB_ne_top : B ≠ ⊤) (hbound : ∫⁻ (x : Vec d), ENNReal.ofReal (vecNormSq (F x)) ∂normalizedCubeMeasure Q ≤ B) : cubeLpNorm Q 2 F ^ 2 ≤ B.toReal

theorem HCPolySupport.overlapCubeLpNorm_two_sq_eq_lintegral_rpow_enorm_toReal {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] (S : TriadicCube d) (f : Vec d → E) (hf : MeasureTheory.AEStronglyMeasurable f (normalizedOverlapCubeMeasure S)) : overlapCubeLpNorm S 2 f ^ 2 = (∫⁻ (x : Vec d), ‖f x‖ₑ ^ 2 ∂normalizedOverlapCubeMeasure S).toReal

theorem HCPolySupport.overlapCubeLpNorm_two_sq_le_lintegral_ofReal_vecNormSq_toReal_of_le {d : ℕ} {S : TriadicCube d} {F : Vec d → Vec d} {B : ENNReal} (hB_ne_top : B ≠ ⊤) (hbound : ∫⁻ (x : Vec d), ENNReal.ofReal (vecNormSq (F x)) ∂normalizedOverlapCubeMeasure S ≤ B) : overlapCubeLpNorm S 2 F ^ 2 ≤ B.toReal

theorem HCPolySupport.ae_mem_overlapCubeSet_normalizedOverlapCubeMeasure {d : ℕ} (S : TriadicCube d) : ∀ᵐ (x : Vec d) ∂normalizedOverlapCubeMeasure S, x ∈ overlapCubeSet S

theorem HCPolySupport.lintegral_ofReal_vecNormSq_le_of_forall_overlapCubeSet {d : ℕ} {S : TriadicCube d} {F : Vec d → Vec d} {B : ℝ} (hpoint : ∀ x ∈ overlapCubeSet S, vecNormSq (F x) ≤ B) : ∫⁻ (x : Vec d), ENNReal.ofReal (vecNormSq (F x)) ∂normalizedOverlapCubeMeasure S ≤ ENNReal.ofReal B

theorem HCPolySupport.overlapCubeLpNorm_two_sq_le_of_forall_overlapCubeSet_vecNormSq_le {d : ℕ} {S : TriadicCube d} {F : Vec d → Vec d} {B : ℝ} (hB : 0 ≤ B) (hpoint : ∀ x ∈ overlapCubeSet S, vecNormSq (F x) ≤ B) : overlapCubeLpNorm S 2 F ^ 2 ≤ B

theorem HCPolySupport.memLp_cubeMeasure_of_memLp_normalizedCubeMeasure {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] (Q : TriadicCube d) {p : ENNReal} {f : Vec d → E} (hf : MeasureTheory.MemLp f p (normalizedCubeMeasure Q)) : MeasureTheory.MemLp f p (cubeMeasure Q)

theorem HCPolySupport.cubeLpNorm_two_eq_volume_inv_rpow_half_mul_norm_toVectorL2_openCubeSet {d : ℕ} (Q : TriadicCube d) {f : Vec d → Vec d} (hf : MeasureTheory.MemLp f 2 (normalizedCubeMeasure Q)) : cubeLpNorm Q 2 f = (cubeVolume Q)⁻¹ ^ (1 / 2) * ‖toVectorL2 ⋯‖

Exact normalized-to-unnormalized vector L² conversion on an open cube.

theorem HCPolySupport.memLp_overlapCubeMeasure_of_memLp_normalizedOverlapCubeMeasure {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] (S : TriadicCube d) {p : ENNReal} {f : Vec d → E} (hf : MeasureTheory.MemLp f p (normalizedOverlapCubeMeasure S)) : MeasureTheory.MemLp f p (overlapCubeMeasure S)

theorem HCPolySupport.memL2On_openOverlapCubeSet_of_memLp_normalizedOverlapCubeMeasure {d : ℕ} (S : TriadicCube d) {f : Vec d → ℝ} (hf : MeasureTheory.MemLp f 2 (normalizedOverlapCubeMeasure S)) : MemL2On (openOverlapCubeSet S) f

theorem HCPolySupport.memVectorL2_openOverlapCubeSet_of_memLp_normalizedOverlapCubeMeasure {d : ℕ} (S : TriadicCube d) {f : Vec d → Vec d} (hf : MeasureTheory.MemLp f 2 (normalizedOverlapCubeMeasure S)) : MemVectorL2 (openOverlapCubeSet S) f

theorem HCPolySupport.memL2On_openOverlapCubeSet_normalizedOverlapCubeMeasure {d : ℕ} {S : TriadicCube d} {f : Vec d → ℝ} (hf : MemL2On (openOverlapCubeSet S) f) : MeasureTheory.MemLp f 2 (normalizedOverlapCubeMeasure S)

theorem HCPolySupport.memVectorL2_openOverlapCubeSet_normalizedOverlapCubeMeasure {d : ℕ} {S : TriadicCube d} {f : Vec d → Vec d} (hf : MemVectorL2 (openOverlapCubeSet S) f) : MeasureTheory.MemLp f 2 (normalizedOverlapCubeMeasure S)

theorem HCPolySupport.overlapCubeLpNorm_two_eq_volume_inv_rpow_half_mul_norm_toScalarL2_openOverlapCubeSet {d : ℕ} (S : TriadicCube d) {f : Vec d → ℝ} (hf : MeasureTheory.MemLp f 2 (normalizedOverlapCubeMeasure S)) : overlapCubeLpNorm S 2 f = (overlapCubeVolume S)⁻¹ ^ (1 / 2) * ‖toScalarL2 ⋯‖

Exact normalized-to-unnormalized L² conversion on an open overlapping cube.

theorem HCPolySupport.norm_toScalarL2_openOverlapCubeSet_eq_volume_rpow_half_mul_overlapCubeLpNorm_two {d : ℕ} (S : TriadicCube d) {f : Vec d → ℝ} (hf : MeasureTheory.MemLp f 2 (normalizedOverlapCubeMeasure S)) : ‖toScalarL2 ⋯‖ = overlapCubeVolume S ^ (1 / 2) * overlapCubeLpNorm S 2 f

theorem HCPolySupport.overlapCubeLpNorm_two_eq_volume_inv_rpow_half_mul_norm_toVectorL2_openOverlapCubeSet {d : ℕ} (S : TriadicCube d) {f : Vec d → Vec d} (hf : MeasureTheory.MemLp f 2 (normalizedOverlapCubeMeasure S)) : overlapCubeLpNorm S 2 f = (overlapCubeVolume S)⁻¹ ^ (1 / 2) * ‖toVectorL2 ⋯‖

Exact normalized-to-unnormalized vector L² conversion on an open overlapping cube.

theorem HCPolySupport.overlapCubeLpNorm_two_sub_overlapCubeAverage_le {d : ℕ} (S : TriadicCube d) (u : H1Function (openOverlapCubeSet S)) : (overlapCubeLpNorm S 2 fun (x : Vec d) => u.toFun x - overlapCubeAverage S fun (y : Vec d) => u.toFun y) ≤ (overlapCubeVolume S)⁻¹ ^ (1 / 2) * (overlapCubeScaleFactor S * (originCubeMeanZeroH1CoerciveEstimate d 0).constantValue * ‖u.gradToVectorL2‖)

theorem HCPolySupport.overlapCubeLpNorm_two_sub_overlapCubeAverage_le_scale_mul_grad {d : ℕ} (S : TriadicCube d) (u : H1Function (openOverlapCubeSet S)) : (overlapCubeLpNorm S 2 fun (x : Vec d) => u.toFun x - overlapCubeAverage S fun (y : Vec d) => u.toFun y) ≤ overlapCubeScaleFactor S * (originCubeMeanZeroH1CoerciveEstimate d 0).constantValue * overlapCubeLpNorm S 2 u.grad