Coarse-graining support: Support.Sobolev.W1p.Dilation

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

noncomputable def HCPolySupport.W1pFunction.dilate {d : ℕ} {U : Set (Vec d)} {p : ENNReal} {a : ℝ} (ha : 0 < a) (u : W1pFunction U p) : W1pFunction (a • U) p

Push a scalar W^{1,p}(U) witness forward to W^{1,p}(a • U) by the positive dilation x ↦ a⁻¹ x. The weak gradient has the corresponding chain-rule factor a⁻¹.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem HCPolySupport.W1pFunction.dilate_toFun {d : ℕ} {U : Set (Vec d)} {p : ENNReal} {a : ℝ} (ha : 0 < a) (u : W1pFunction U p) (x : Vec d) : (dilate ha u).toFun x = u.toFun (a⁻¹ • x)

@[simp]

theorem HCPolySupport.W1pFunction.dilate_grad {d : ℕ} {U : Set (Vec d)} {p : ENNReal} {a : ℝ} (ha : 0 < a) (u : W1pFunction U p) (x : Vec d) : (dilate ha u).grad x = a⁻¹ • u.grad (a⁻¹ • x)

noncomputable def HCPolySupport.W1pFunction.unscale {d : ℕ} {U : Set (Vec d)} {p : ENNReal} {a : ℝ} (ha : 0 < a) (u : W1pFunction (a • U) p) : W1pFunction U p

Pull a scalar W^{1,p}(a • U) witness back to W^{1,p}(U) by precomposition with x ↦ a • x. Its weak gradient is a • ∇u(a • x).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem HCPolySupport.W1pFunction.unscale_toFun {d : ℕ} {U : Set (Vec d)} {p : ENNReal} {a : ℝ} (ha : 0 < a) (u : W1pFunction (a • U) p) (x : Vec d) : (unscale ha u).toFun x = u.toFun (a • x)

@[simp]

theorem HCPolySupport.W1pFunction.unscale_grad {d : ℕ} {U : Set (Vec d)} {p : ENNReal} {a : ℝ} (ha : 0 < a) (u : W1pFunction (a • U) p) (x : Vec d) : (unscale ha u).grad x = a • u.grad (a • x)

noncomputable def HCPolySupport.W1pFunction.dilationLpFactor (d : ℕ) (p : ENNReal) (a : ℝ) : ℝ

The common L^p measure factor in a positive dilation of Vec d.

Equations

• HCPolySupport.W1pFunction.dilationLpFactor d p a = (ENNReal.ofReal (a⁻¹ ^ d)⁻¹ ^ (1 / p).toReal).toReal

theorem HCPolySupport.W1pFunction.dilationLpFactor_pos (d : ℕ) (p : ENNReal) {a : ℝ} (ha : 0 < a) : 0 < dilationLpFactor d p a

Positivity of the finite-dimensional dilation norm factor.

theorem HCPolySupport.W1pFunction.eLpNorm_comp_smul_eq {d : ℕ} {U : Set (Vec d)} {p : ENNReal} {a : ℝ} (ha : 0 < a) (hp_top : p ≠ ⊤) {f : Vec d → ℝ} (hf : MeasureTheory.AEStronglyMeasurable f (volumeMeasureOn (a • U))) : MeasureTheory.eLpNorm (fun (x : Vec d) => f (a • x)) p (volumeMeasureOn U) = ENNReal.ofReal (a ^ d)⁻¹ ^ (1 / p).toReal * MeasureTheory.eLpNorm f p (volumeMeasureOn (a • U))

Change of variables for an L^p norm under the forward positive dilation.

theorem HCPolySupport.W1pFunction.eLpNorm_unscale_toFun {d : ℕ} {U : Set (Vec d)} {p : ENNReal} {a : ℝ} (ha : 0 < a) (hp_top : p ≠ ⊤) (u : W1pFunction (a • U) p) : MeasureTheory.eLpNorm (unscale ha u).toFun p (volumeMeasureOn U) = ENNReal.ofReal (a ^ d)⁻¹ ^ (1 / p).toReal * MeasureTheory.eLpNorm u.toFun p (volumeMeasureOn (a • U))

The eLpNorm of a value representative after pulling it back by dilation.

theorem HCPolySupport.W1pFunction.valueLpSeminorm_unscale_eq {d : ℕ} {U : Set (Vec d)} {p : ENNReal} {a : ℝ} (ha : 0 < a) (hp_top : p ≠ ⊤) (u : W1pFunction (a • U) p) : (unscale ha u).valueLpSeminorm = dilationLpFactor d p a⁻¹ * u.valueLpSeminorm

The scalar value L^p seminorm under pullback by positive dilation.

theorem HCPolySupport.W1pFunction.eLpNorm_unscale_gradCoord {d : ℕ} {U : Set (Vec d)} {p : ENNReal} {a : ℝ} (ha : 0 < a) (hp_top : p ≠ ⊤) (u : W1pFunction (a • U) p) (i : Fin d) : MeasureTheory.eLpNorm (fun (x : Vec d) => (unscale ha u).grad x i) p (volumeMeasureOn U) = ENNReal.ofReal a * (ENNReal.ofReal (a ^ d)⁻¹ ^ (1 / p).toReal * MeasureTheory.eLpNorm (fun (x : Vec d) => u.grad x i) p (volumeMeasureOn (a • U)))

The eLpNorm of one weak-gradient coordinate after dilation pullback.

theorem HCPolySupport.W1pFunction.gradCoordLpSeminorm_unscale_eq {d : ℕ} {U : Set (Vec d)} {p : ENNReal} {a : ℝ} (ha : 0 < a) (hp_top : p ≠ ⊤) (u : W1pFunction (a • U) p) (i : Fin d) : (unscale ha u).gradCoordLpSeminorm i = a * dilationLpFactor d p a⁻¹ * u.gradCoordLpSeminorm i

The coordinate gradient L^p seminorm under pullback by positive dilation.

theorem HCPolySupport.W1pFunction.gradientCoordLpSeminormSum_unscale_eq {d : ℕ} {U : Set (Vec d)} {p : ENNReal} {a : ℝ} (ha : 0 < a) (hp_top : p ≠ ⊤) (u : W1pFunction (a • U) p) : (unscale ha u).gradientCoordLpSeminormSum = a * dilationLpFactor d p a⁻¹ * u.gradientCoordLpSeminormSum

The coordinate-sum gradient L^p seminorm under dilation pullback.

theorem HCPolySupport.W1pFunction.integralAverage_unscale_eq {d : ℕ} {U : Set (Vec d)} {p : ENNReal} {a : ℝ} (ha : 0 < a) (u : W1pFunction (a • U) p) : integralAverage U (unscale ha u).toFun = integralAverage (a • U) u.toFun

Integral averages commute with the pullback of a scalar witness by positive dilation.

theorem HCPolySupport.W1pFunction.meanZeroOn_unscale {d : ℕ} {U : Set (Vec d)} {p : ENNReal} {a : ℝ} (ha : 0 < a) (u : W1pFunction (a • U) p) (hmean : MeanZeroOn (a • U) u.toFun) : MeanZeroOn U (unscale ha u).toFun

Pullback by a positive dilation preserves the zero-average condition.

theorem HCPolySupport.W1pFunction.subAverageLpSeminorm_unscale_eq {d : ℕ} {U : Set (Vec d)} {p : ENNReal} {a : ℝ} (ha : 0 < a) (hp_top : p ≠ ⊤) (u : W1pFunction (a • U) p) : (unscale ha u).subAverageLpSeminorm = dilationLpFactor d p a⁻¹ * u.subAverageLpSeminorm

The mean-subtracted scalar L^p seminorm under pullback by positive dilation.

theorem HCPolySupport.W1pFunction.eLpNorm_comp_dilate_eq {d : ℕ} {U : Set (Vec d)} {p : ENNReal} {a : ℝ} (ha : 0 < a) (hp_top : p ≠ ⊤) {f : Vec d → ℝ} (hf : MeasureTheory.AEStronglyMeasurable f (volumeMeasureOn U)) : MeasureTheory.eLpNorm (fun (x : Vec d) => f (a⁻¹ • x)) p (volumeMeasureOn (a • U)) = ENNReal.ofReal (a⁻¹ ^ d)⁻¹ ^ (1 / p).toReal * MeasureTheory.eLpNorm f p (volumeMeasureOn U)

Change of variables for an L^p norm under the inverse positive dilation. The assumption is measurability rather than MemLp, so it also applies to the mean-subtracted representative in the Poincare seminorm.

theorem HCPolySupport.W1pFunction.eLpNorm_dilate_toFun {d : ℕ} {U : Set (Vec d)} {p : ENNReal} {a : ℝ} (ha : 0 < a) (hp_top : p ≠ ⊤) (u : W1pFunction U p) : MeasureTheory.eLpNorm (dilate ha u).toFun p (volumeMeasureOn (a • U)) = ENNReal.ofReal (a⁻¹ ^ d)⁻¹ ^ (1 / p).toReal * MeasureTheory.eLpNorm u.toFun p (volumeMeasureOn U)

The eLpNorm of the value representative after a positive dilation.

theorem HCPolySupport.W1pFunction.valueLpSeminorm_dilate_eq {d : ℕ} {U : Set (Vec d)} {p : ENNReal} {a : ℝ} (ha : 0 < a) (hp_top : p ≠ ⊤) (u : W1pFunction U p) : (dilate ha u).valueLpSeminorm = dilationLpFactor d p a * u.valueLpSeminorm

The scalar value L^p seminorm under positive dilation.

theorem HCPolySupport.W1pFunction.eLpNorm_dilate_gradCoord {d : ℕ} {U : Set (Vec d)} {p : ENNReal} {a : ℝ} (ha : 0 < a) (hp_top : p ≠ ⊤) (u : W1pFunction U p) (i : Fin d) : MeasureTheory.eLpNorm (fun (x : Vec d) => (dilate ha u).grad x i) p (volumeMeasureOn (a • U)) = ENNReal.ofReal a⁻¹ * (ENNReal.ofReal (a⁻¹ ^ d)⁻¹ ^ (1 / p).toReal * MeasureTheory.eLpNorm (fun (x : Vec d) => u.grad x i) p (volumeMeasureOn U))

The eLpNorm of one weak-gradient coordinate after positive dilation.

theorem HCPolySupport.W1pFunction.gradCoordLpSeminorm_dilate_eq {d : ℕ} {U : Set (Vec d)} {p : ENNReal} {a : ℝ} (ha : 0 < a) (hp_top : p ≠ ⊤) (u : W1pFunction U p) (i : Fin d) : (dilate ha u).gradCoordLpSeminorm i = a⁻¹ * dilationLpFactor d p a * u.gradCoordLpSeminorm i

The coordinate gradient L^p seminorm under positive dilation.

theorem HCPolySupport.W1pFunction.gradientCoordLpSeminormSum_dilate_eq {d : ℕ} {U : Set (Vec d)} {p : ENNReal} {a : ℝ} (ha : 0 < a) (hp_top : p ≠ ⊤) (u : W1pFunction U p) : (dilate ha u).gradientCoordLpSeminormSum = a⁻¹ * dilationLpFactor d p a * u.gradientCoordLpSeminormSum

The coordinate-sum gradient L^p seminorm under positive dilation.

theorem HCPolySupport.W1pFunction.integralAverage_dilate_eq {d : ℕ} {U : Set (Vec d)} {p : ENNReal} {a : ℝ} (ha : 0 < a) (u : W1pFunction U p) : integralAverage (a • U) (dilate ha u).toFun = integralAverage U u.toFun

Integral averages commute with positive dilation of a scalar witness.

theorem HCPolySupport.W1pFunction.subAverageLpSeminorm_dilate_eq {d : ℕ} {U : Set (Vec d)} {p : ENNReal} {a : ℝ} (ha : 0 < a) (hp_top : p ≠ ⊤) (u : W1pFunction U p) : (dilate ha u).subAverageLpSeminorm = dilationLpFactor d p a * u.subAverageLpSeminorm

The mean-subtracted scalar L^p seminorm under positive dilation.