Coarse-graining support: Support.Sobolev.Foundations.PoincareW1p.Core

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

theorem HCPolySupport.W1pFunction.subAverageLpSeminorm_le_poincare_mul_gradientCoordLpSeminormSum {d : ℕ} {U : Set (Vec d)} [NeZero d] (hU : IsOpenBoundedConvexDomain U) {q : ℝ} (hq : 1 < q) (hvol : 0 < (MeasureTheory.volume U).toReal) (u : W1pFunction U (ENNReal.ofReal q)) : u.subAverageLpSeminorm ≤ smoothPoincareLpConst hU * u.gradientCoordLpSeminormSum

theorem HCPolySupport.W1pFunction.exists_subAverage_poincare_constant_of_isOpenBoundedConvexDomain {d : ℕ} {U : Set (Vec d)} [NeZero d] (hU : IsOpenBoundedConvexDomain U) {q : ℝ} (hq : 1 < q) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (u : W1pFunction U (ENNReal.ofReal q)), u.subAverageLpSeminorm ≤ C * u.gradientCoordLpSeminormSum

theorem HCPolySupport.W1pFunction.integralAverage_eq_zero_of_meanZero {d : ℕ} {U : Set (Vec d)} {p : ENNReal} (u : W1pFunction U p) (hmean : MeanZeroOn U u.toFun) : integralAverage U u.toFun = 0

theorem HCPolySupport.W1pFunction.subAverageLpSeminorm_eq_valueLpSeminorm_of_meanZero {d : ℕ} {U : Set (Vec d)} {p : ENNReal} (u : W1pFunction U p) (hmean : MeanZeroOn U u.toFun) : u.subAverageLpSeminorm = u.valueLpSeminorm

theorem HCPolySupport.W1pFunction.valueLpSeminorm_eq_zero_of_volume_toReal_eq_zero {d : ℕ} {U : Set (Vec d)} {p : ENNReal} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hvol : (MeasureTheory.volume U).toReal = 0) (u : W1pFunction U p) : u.valueLpSeminorm = 0

structure HCPolySupport.W1pMeanZeroFunction {d : ℕ} (U : Set (Vec d)) (p : ENNReal) : Type

Mean-zero W^{1,p}(U) functions, represented by a chosen witness together with the zero-average condition.

• toW1pFunction : W1pFunction U p

  The W^{1,p} function underlying the mean-zero Sobolev function.

• meanZero : MeanZeroOn U self.toW1pFunction.toFun

@[instance_reducible]

instance HCPolySupport.W1pMeanZeroFunction.instCoeW1pFunction {d : ℕ} {U : Set (Vec d)} {p : ENNReal} : Coe (W1pMeanZeroFunction U p) (W1pFunction U p)

Equations

• HCPolySupport.W1pMeanZeroFunction.instCoeW1pFunction = { coe := fun (u : HCPolySupport.W1pMeanZeroFunction U p) => u.toW1pFunction }

@[instance_reducible]

instance HCPolySupport.W1pMeanZeroFunction.instCoeFunForallVecReal {d : ℕ} {U : Set (Vec d)} {p : ENNReal} : CoeFun (W1pMeanZeroFunction U p) fun (x : W1pMeanZeroFunction U p) => Vec d → ℝ

Equations

• HCPolySupport.W1pMeanZeroFunction.instCoeFunForallVecReal = { coe := fun (u : HCPolySupport.W1pMeanZeroFunction U p) => u.toW1pFunction.toFun }

@[simp]

theorem HCPolySupport.W1pMeanZeroFunction.coe_mk {d : ℕ} {U : Set (Vec d)} {p : ENNReal} (u : W1pFunction U p) (hmean : MeanZeroOn U u.toFun) : { toW1pFunction := u, meanZero := hmean }.toW1pFunction = u

theorem HCPolySupport.W1pMeanZeroFunction.ext {d : ℕ} {U : Set (Vec d)} {p : ENNReal} {u v : W1pMeanZeroFunction U p} (htoW1p : u.toW1pFunction = v.toW1pFunction) : u = v

theorem HCPolySupport.W1pMeanZeroFunction.ext_iff {d : ℕ} {U : Set (Vec d)} {p : ENNReal} {u v : W1pMeanZeroFunction U p} : u = v ↔ u.toW1pFunction = v.toW1pFunction

noncomputable def HCPolySupport.W1pMeanZeroFunction.valueLpSeminorm {d : ℕ} {U : Set (Vec d)} {p : ENNReal} (u : W1pMeanZeroFunction U p) : ℝ

The scalar L^p(U) seminorm of a mean-zero W^{1,p} function.

Equations

• u.valueLpSeminorm = u.toW1pFunction.valueLpSeminorm

noncomputable def HCPolySupport.W1pMeanZeroFunction.gradientCoordLpSeminormSum {d : ℕ} {U : Set (Vec d)} {p : ENNReal} (u : W1pMeanZeroFunction U p) : ℝ

Coordinate-sum gradient seminorm of a mean-zero W^{1,p} function.

Equations

• u.gradientCoordLpSeminormSum = u.toW1pFunction.gradientCoordLpSeminormSum

theorem HCPolySupport.W1pMeanZeroFunction.valueLpSeminorm_nonneg {d : ℕ} {U : Set (Vec d)} {p : ENNReal} (u : W1pMeanZeroFunction U p) : 0 ≤ u.valueLpSeminorm

theorem HCPolySupport.W1pMeanZeroFunction.gradientCoordLpSeminormSum_nonneg {d : ℕ} {U : Set (Vec d)} {p : ENNReal} (u : W1pMeanZeroFunction U p) : 0 ≤ u.gradientCoordLpSeminormSum

theorem HCPolySupport.W1pMeanZeroFunction.subAverageLpSeminorm_eq_valueLpSeminorm {d : ℕ} {U : Set (Vec d)} {p : ENNReal} (u : W1pMeanZeroFunction U p) : u.toW1pFunction.subAverageLpSeminorm = u.valueLpSeminorm

theorem HCPolySupport.W1pMeanZeroFunction.valueLpSeminorm_eq_zero_of_dim_zero {p : ENNReal} {U : Set (Vec 0)} (hvol : 0 < (MeasureTheory.volume U).toReal) (u : W1pMeanZeroFunction U p) : u.valueLpSeminorm = 0

structure HCPolySupport.W1pPoincareEstimate {d : ℕ} (U : Set (Vec d)) (p : ENNReal) : Type

A bundled finite-p mean-zero Poincare estimate for the W^{1,p} layer.

• constantValue : ℝ

  The nonnegative constant bounding a mean-zero W^{1,p} function's value seminorm by the sum of its coordinate gradient seminorms.

• constant_nonneg : 0 ≤ self.constantValue
• bound (u : W1pMeanZeroFunction U p) : u.valueLpSeminorm ≤ self.constantValue * u.gradientCoordLpSeminormSum

theorem HCPolySupport.W1pPoincareEstimate.bound_subAverage {d : ℕ} {U : Set (Vec d)} {p : ENNReal} (hC : W1pPoincareEstimate U p) (u : W1pFunction U p) (hmean : MeanZeroOn U u.toFun) : u.subAverageLpSeminorm ≤ hC.constantValue * u.gradientCoordLpSeminormSum

noncomputable def HCPolySupport.w1pPoincareEstimateOfOpenBoundedConvexDomain {d : ℕ} {U : Set (Vec d)} {q : ℝ} (hU : IsOpenBoundedConvexDomain U) (hq : 1 < q) : W1pPoincareEstimate U (ENNReal.ofReal q)

Bounded open convex domains satisfy the mean-zero finite-p Poincare estimate for every real exponent 1 < p < ∞, packaged on the witness-based W1pFunction API.

Equations

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