Coarse-graining support: Support.Sobolev.NegativeSobolev

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

Normalized negative Sobolev seminorms

The two Chapter 1 dual seminorms use the normalized pairing prescribed by RULING-0001. The first test carrier is literally Mathlib's smooth compactly supported test-function space; the second uses genuine weak W^{1,p} witnesses with zero normalized average.

@[reducible, inline]

noncomputable abbrev HCPolySupport.NegativeSobolev.domain {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (hne : U.Nonempty) : BoundedMeasurableDomain d

The positive-finite normalized domain induced by the public convex carrier.

Equations

• HCPolySupport.NegativeSobolev.domain hU hne = hU.toBoundedMeasurableDomain hne

@[reducible, inline]

abbrev HCPolySupport.NegativeSobolev.SmoothTestFunction {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) : Type

The literal C_c^∞(U) carrier for the zero-boundary dual seminorm.

Equations

• HCPolySupport.NegativeSobolev.SmoothTestFunction hU = HCPolySupport.SmoothCompactSupportFunction hU.toOpens

noncomputable def HCPolySupport.NegativeSobolev.smoothTestSeminorm {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (hne : U.Nonempty) (p : ENNReal) (hp_one : 1 < p) (hp_top : p ≠ ⊤) (φ : SmoothTestFunction hU) : ℝ

The exact normalized gradient seminorm imposed on smooth tests.

Equations

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

def HCPolySupport.NegativeSobolev.SmoothTestAdmissible {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (hne : U.Nonempty) (p : ENNReal) (hp_one : 1 < p) (hp_top : p ≠ ⊤) (φ : SmoothTestFunction hU) : Prop

The smooth tests in the unit normalized gradient-seminorm ball.

Equations

• HCPolySupport.NegativeSobolev.SmoothTestAdmissible hU hne p hp_one hp_top φ = (HCPolySupport.NegativeSobolev.smoothTestSeminorm hU hne p hp_one hp_top φ ≤ 1)

structure HCPolySupport.NegativeSobolev.MeanZeroW1pTestFunction {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (hne : U.Nonempty) (p : ENNReal) : Type

A genuine weak W^{1,p}(U) witness with zero normalized average.

• toW1pFunction : W1pFunction U p

  The weak-Sobolev function used as a mean-zero test.

• normalizedIntegral_eq_zero : ∫ (x : Vec d), self.toW1pFunction.toFun x ∂(domain hU hne).normalizedVolume = 0

noncomputable def HCPolySupport.NegativeSobolev.meanZeroTestSeminorm {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (hne : U.Nonempty) (p : ENNReal) (hp_one : 1 < p) (hp_top : p ≠ ⊤) (φ : MeanZeroW1pTestFunction hU hne p) : ℝ

The exact normalized gradient seminorm imposed on mean-zero tests.

Equations

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

def HCPolySupport.NegativeSobolev.MeanZeroTestAdmissible {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (hne : U.Nonempty) (p : ENNReal) (hp_one : 1 < p) (hp_top : p ≠ ⊤) (φ : MeanZeroW1pTestFunction hU hne p) : Prop

The mean-zero weak tests in the unit normalized gradient-seminorm ball.

Equations

• HCPolySupport.NegativeSobolev.MeanZeroTestAdmissible hU hne p hp_one hp_top φ = (HCPolySupport.NegativeSobolev.meanZeroTestSeminorm hU hne p hp_one hp_top φ ≤ 1)

theorem HCPolySupport.NegativeSobolev.smoothTest_memLp_normalized {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (hne : U.Nonempty) (p : ENNReal) (φ : SmoothTestFunction hU) : MeasureTheory.MemLp (⇑φ) p (domain hU hne).normalizedVolume

theorem HCPolySupport.NegativeSobolev.meanZeroTest_memLp_normalized {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (hne : U.Nonempty) (p : ENNReal) (φ : MeanZeroW1pTestFunction hU hne p) : MeasureTheory.MemLp φ.toW1pFunction.toFun p (domain hU hne).normalizedVolume

theorem HCPolySupport.NegativeSobolev.pairing_integrable {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (hne : U.Nonempty) (p : ENNReal) (hp_one : 1 < p) (f : Vec d → ℝ) (hf : MeasureTheory.MemLp f p.conjExponent (domain hU hne).normalizedVolume) (g : Vec d → ℝ) (hg : MeasureTheory.MemLp g p (domain hU hne).normalizedVolume) : MeasureTheory.Integrable (fun (x : Vec d) => f x * g x) (domain hU hne).normalizedVolume

noncomputable def HCPolySupport.NegativeSobolev.normalizedPairing {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (hne : U.Nonempty) (p : ENNReal) (hp_one : 1 < p) (f : Vec d → ℝ) (hf : MeasureTheory.MemLp f p.conjExponent (domain hU hne).normalizedVolume) (g : Vec d → ℝ) (hg : MeasureTheory.MemLp g p (domain hU hne).normalizedVolume) : ℝ

The normalized pairing fint_U f g. Product integrability is derived from the two MemLp witnesses by Hölder, never supplied by the caller.

Equations

• HCPolySupport.NegativeSobolev.normalizedPairing hU hne p hp_one f hf g hg = (HCPolySupport.NegativeSobolev.domain hU hne).pairing f g ⋯

noncomputable def HCPolySupport.NegativeSobolev.smoothPairing {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (hne : U.Nonempty) (p : ENNReal) (hp_one : 1 < p) (f : Vec d → ℝ) (hf : MeasureTheory.MemLp f p.conjExponent (domain hU hne).normalizedVolume) (φ : SmoothTestFunction hU) : ℝ

The normalized pairing against a literal smooth compactly supported test.

Equations

• HCPolySupport.NegativeSobolev.smoothPairing hU hne p hp_one f hf φ = HCPolySupport.NegativeSobolev.normalizedPairing hU hne p hp_one f hf ⇑φ ⋯

noncomputable def HCPolySupport.NegativeSobolev.meanZeroPairing {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (hne : U.Nonempty) (p : ENNReal) (hp_one : 1 < p) (f : Vec d → ℝ) (hf : MeasureTheory.MemLp f p.conjExponent (domain hU hne).normalizedVolume) (φ : MeanZeroW1pTestFunction hU hne p) : ℝ

The normalized pairing against a genuine mean-zero weak test.

Equations

• HCPolySupport.NegativeSobolev.meanZeroPairing hU hne p hp_one f hf φ = HCPolySupport.NegativeSobolev.normalizedPairing hU hne p hp_one f hf φ.toW1pFunction.toFun ⋯

noncomputable def HCPolySupport.NegativeSobolev.smoothNegativeSobolevSeminorm {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (hne : U.Nonempty) (p : ENNReal) (hp_one : 1 < p) (hp_top : p ≠ ⊤) (f : Vec d → ℝ) (hf : MeasureTheory.MemLp f p.conjExponent (domain hU hne).normalizedVolume) : ENNReal

The signed Chapter 1 zero-boundary negative Sobolev seminorm.

Equations

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

noncomputable def HCPolySupport.NegativeSobolev.meanZeroNegativeSobolevSeminorm {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (hne : U.Nonempty) (p : ENNReal) (hp_one : 1 < p) (hp_top : p ≠ ⊤) (f : Vec d → ℝ) (hf : MeasureTheory.MemLp f p.conjExponent (domain hU hne).normalizedVolume) : ENNReal

The signed Chapter 1 mean-zero negative Sobolev seminorm.

Equations

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

noncomputable def HCPolySupport.NegativeSobolev.smoothNegativeSobolevAbsSeminorm {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (hne : U.Nonempty) (p : ENNReal) (hp_one : 1 < p) (hp_top : p ≠ ⊤) (f : Vec d → ℝ) (hf : MeasureTheory.MemLp f p.conjExponent (domain hU hne).normalizedVolume) : ENNReal

The absolute-pairing form of the zero-boundary seminorm.

Equations

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

noncomputable def HCPolySupport.NegativeSobolev.meanZeroNegativeSobolevAbsSeminorm {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (hne : U.Nonempty) (p : ENNReal) (hp_one : 1 < p) (hp_top : p ≠ ⊤) (f : Vec d → ℝ) (hf : MeasureTheory.MemLp f p.conjExponent (domain hU hne).normalizedVolume) : ENNReal

The absolute-pairing form of the mean-zero seminorm.

Equations

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

Transparent characterizations

theorem HCPolySupport.NegativeSobolev.smoothNegativeSobolevSeminorm_eq_iSup {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (hne : U.Nonempty) (p : ENNReal) (hp_one : 1 < p) (hp_top : p ≠ ⊤) (f : Vec d → ℝ) (hf : MeasureTheory.MemLp f p.conjExponent (domain hU hne).normalizedVolume) : smoothNegativeSobolevSeminorm hU hne p hp_one hp_top f hf = ⨆ (φ : { φ : SmoothTestFunction hU // SmoothTestAdmissible hU hne p hp_one hp_top φ }), ENNReal.ofReal (smoothPairing hU hne p hp_one f hf ↑φ)

theorem HCPolySupport.NegativeSobolev.meanZeroNegativeSobolevSeminorm_eq_iSup {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (hne : U.Nonempty) (p : ENNReal) (hp_one : 1 < p) (hp_top : p ≠ ⊤) (f : Vec d → ℝ) (hf : MeasureTheory.MemLp f p.conjExponent (domain hU hne).normalizedVolume) : meanZeroNegativeSobolevSeminorm hU hne p hp_one hp_top f hf = ⨆ (φ : { φ : MeanZeroW1pTestFunction hU hne p // MeanZeroTestAdmissible hU hne p hp_one hp_top φ }), ENNReal.ofReal (meanZeroPairing hU hne p hp_one f hf ↑φ)

theorem HCPolySupport.NegativeSobolev.smoothNegativeSobolevAbsSeminorm_eq_iSup {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (hne : U.Nonempty) (p : ENNReal) (hp_one : 1 < p) (hp_top : p ≠ ⊤) (f : Vec d → ℝ) (hf : MeasureTheory.MemLp f p.conjExponent (domain hU hne).normalizedVolume) : smoothNegativeSobolevAbsSeminorm hU hne p hp_one hp_top f hf = ⨆ (φ : { φ : SmoothTestFunction hU // SmoothTestAdmissible hU hne p hp_one hp_top φ }), ENNReal.ofReal |smoothPairing hU hne p hp_one f hf ↑φ|

theorem HCPolySupport.NegativeSobolev.meanZeroNegativeSobolevAbsSeminorm_eq_iSup {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (hne : U.Nonempty) (p : ENNReal) (hp_one : 1 < p) (hp_top : p ≠ ⊤) (f : Vec d → ℝ) (hf : MeasureTheory.MemLp f p.conjExponent (domain hU hne).normalizedVolume) : meanZeroNegativeSobolevAbsSeminorm hU hne p hp_one hp_top f hf = ⨆ (φ : { φ : MeanZeroW1pTestFunction hU hne p // MeanZeroTestAdmissible hU hne p hp_one hp_top φ }), ENNReal.ofReal |meanZeroPairing hU hne p hp_one f hf ↑φ|

Test-class symmetry

noncomputable def HCPolySupport.NegativeSobolev.negW1pFunction {d : ℕ} {U : Set (Vec d)} {p : ENNReal} (u : W1pFunction U p) : W1pFunction U p

The W^{1,p} function with value and weak gradient equal to the negatives of those of u.

Equations

• HCPolySupport.NegativeSobolev.negW1pFunction u = { toFun := -u.toFun, grad := -u.grad, memLp := ⋯, gradMemLp := ⋯, hasWeakGradient := ⋯ }

noncomputable def HCPolySupport.NegativeSobolev.zeroW1pFunction {d : ℕ} {U : Set (Vec d)} (p : ENNReal) : W1pFunction U p

The zero W^{1,p} function with zero weak gradient.

Equations

• HCPolySupport.NegativeSobolev.zeroW1pFunction p = { toFun := 0, grad := 0, memLp := ⋯, gradMemLp := ⋯, hasWeakGradient := ⋯ }

noncomputable def HCPolySupport.NegativeSobolev.smoothTestZero {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) : SmoothTestFunction hU

Zero belongs to the literal smooth test carrier.

Equations

• HCPolySupport.NegativeSobolev.smoothTestZero hU = 0

theorem HCPolySupport.NegativeSobolev.smoothTestAdmissible_zero {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (hne : U.Nonempty) (p : ENNReal) (hp_one : 1 < p) (hp_top : p ≠ ⊤) : SmoothTestAdmissible hU hne p hp_one hp_top (smoothTestZero hU)

theorem HCPolySupport.NegativeSobolev.smoothTestAdmissible_neg {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (hne : U.Nonempty) (p : ENNReal) (hp_one : 1 < p) (hp_top : p ≠ ⊤) {φ : SmoothTestFunction hU} (hφ : SmoothTestAdmissible hU hne p hp_one hp_top φ) : SmoothTestAdmissible hU hne p hp_one hp_top (-φ)

noncomputable def HCPolySupport.NegativeSobolev.MeanZeroW1pTestFunction.neg {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (hne : U.Nonempty) {p : ENNReal} (φ : MeanZeroW1pTestFunction hU hne p) : MeanZeroW1pTestFunction hU hne p

Negation preserves genuine mean-zero weak tests.

Equations

• HCPolySupport.NegativeSobolev.MeanZeroW1pTestFunction.neg hU hne φ = { toW1pFunction := HCPolySupport.NegativeSobolev.negW1pFunction φ.toW1pFunction, normalizedIntegral_eq_zero := ⋯ }

theorem HCPolySupport.NegativeSobolev.meanZeroTestSeminorm_neg {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (hne : U.Nonempty) (p : ENNReal) (hp_one : 1 < p) (hp_top : p ≠ ⊤) (φ : MeanZeroW1pTestFunction hU hne p) : meanZeroTestSeminorm hU hne p hp_one hp_top (MeanZeroW1pTestFunction.neg hU hne φ) = meanZeroTestSeminorm hU hne p hp_one hp_top φ

noncomputable def HCPolySupport.NegativeSobolev.MeanZeroW1pTestFunction.zero {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (hne : U.Nonempty) (p : ENNReal) : MeanZeroW1pTestFunction hU hne p

Zero belongs to the mean-zero weak test carrier.

Equations

• HCPolySupport.NegativeSobolev.MeanZeroW1pTestFunction.zero hU hne p = { toW1pFunction := HCPolySupport.NegativeSobolev.zeroW1pFunction p, normalizedIntegral_eq_zero := ⋯ }

theorem HCPolySupport.NegativeSobolev.meanZeroTestAdmissible_zero {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (hne : U.Nonempty) (p : ENNReal) (hp_one : 1 < p) (hp_top : p ≠ ⊤) : MeanZeroTestAdmissible hU hne p hp_one hp_top (MeanZeroW1pTestFunction.zero hU hne p)

theorem HCPolySupport.NegativeSobolev.meanZeroTestAdmissible_neg {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (hne : U.Nonempty) (p : ENNReal) (hp_one : 1 < p) (hp_top : p ≠ ⊤) {φ : MeanZeroW1pTestFunction hU hne p} (hφ : MeanZeroTestAdmissible hU hne p hp_one hp_top φ) : MeanZeroTestAdmissible hU hne p hp_one hp_top (MeanZeroW1pTestFunction.neg hU hne φ)

Pairing symmetry and absolute-value characterizations

theorem HCPolySupport.NegativeSobolev.normalizedPairing_neg_right {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (hne : U.Nonempty) (p : ENNReal) (hp_one : 1 < p) (f : Vec d → ℝ) (hf : MeasureTheory.MemLp f p.conjExponent (domain hU hne).normalizedVolume) (g : Vec d → ℝ) (hg : MeasureTheory.MemLp g p (domain hU hne).normalizedVolume) : normalizedPairing hU hne p hp_one f hf (-g) ⋯ = -normalizedPairing hU hne p hp_one f hf g hg

theorem HCPolySupport.NegativeSobolev.smoothPairing_neg {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (hne : U.Nonempty) (p : ENNReal) (hp_one : 1 < p) (f : Vec d → ℝ) (hf : MeasureTheory.MemLp f p.conjExponent (domain hU hne).normalizedVolume) (φ : SmoothTestFunction hU) : smoothPairing hU hne p hp_one f hf (-φ) = -smoothPairing hU hne p hp_one f hf φ

theorem HCPolySupport.NegativeSobolev.meanZeroPairing_neg {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (hne : U.Nonempty) (p : ENNReal) (hp_one : 1 < p) (f : Vec d → ℝ) (hf : MeasureTheory.MemLp f p.conjExponent (domain hU hne).normalizedVolume) (φ : MeanZeroW1pTestFunction hU hne p) : meanZeroPairing hU hne p hp_one f hf (MeanZeroW1pTestFunction.neg hU hne φ) = -meanZeroPairing hU hne p hp_one f hf φ

noncomputable def HCPolySupport.NegativeSobolev.smoothAdmissibleNeg {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (hne : U.Nonempty) (p : ENNReal) (hp_one : 1 < p) (hp_top : p ≠ ⊤) (φ : { φ : SmoothTestFunction hU // SmoothTestAdmissible hU hne p hp_one hp_top φ }) : { φ : SmoothTestFunction hU // SmoothTestAdmissible hU hne p hp_one hp_top φ }

Negation of an admissible smooth test, retaining its negative Sobolev test admissibility.

Equations

• HCPolySupport.NegativeSobolev.smoothAdmissibleNeg hU hne p hp_one hp_top φ = ⟨-↑φ, ⋯⟩

noncomputable def HCPolySupport.NegativeSobolev.meanZeroAdmissibleNeg {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (hne : U.Nonempty) (p : ENNReal) (hp_one : 1 < p) (hp_top : p ≠ ⊤) (φ : { φ : MeanZeroW1pTestFunction hU hne p // MeanZeroTestAdmissible hU hne p hp_one hp_top φ }) : { φ : MeanZeroW1pTestFunction hU hne p // MeanZeroTestAdmissible hU hne p hp_one hp_top φ }

Negation of an admissible mean-zero W^{1,p} test, retaining its zero mean and test admissibility.

Equations

• HCPolySupport.NegativeSobolev.meanZeroAdmissibleNeg hU hne p hp_one hp_top φ = ⟨HCPolySupport.NegativeSobolev.MeanZeroW1pTestFunction.neg hU hne ↑φ, ⋯⟩

theorem HCPolySupport.NegativeSobolev.smoothNegativeSobolevSeminorm_eq_abs {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (hne : U.Nonempty) (p : ENNReal) (hp_one : 1 < p) (hp_top : p ≠ ⊤) (f : Vec d → ℝ) (hf : MeasureTheory.MemLp f p.conjExponent (domain hU hne).normalizedVolume) : smoothNegativeSobolevSeminorm hU hne p hp_one hp_top f hf = smoothNegativeSobolevAbsSeminorm hU hne p hp_one hp_top f hf

theorem HCPolySupport.NegativeSobolev.meanZeroNegativeSobolevSeminorm_eq_abs {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (hne : U.Nonempty) (p : ENNReal) (hp_one : 1 < p) (hp_top : p ≠ ⊤) (f : Vec d → ℝ) (hf : MeasureTheory.MemLp f p.conjExponent (domain hU hne).normalizedVolume) : meanZeroNegativeSobolevSeminorm hU hne p hp_one hp_top f hf = meanZeroNegativeSobolevAbsSeminorm hU hne p hp_one hp_top f hf

Almost-everywhere invariance

theorem HCPolySupport.NegativeSobolev.normalizedPairing_congr_ae {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (hne : U.Nonempty) (p : ENNReal) (hp_one : 1 < p) (f f' : Vec d → ℝ) (hf : MeasureTheory.MemLp f p.conjExponent (domain hU hne).normalizedVolume) (hf' : MeasureTheory.MemLp f' p.conjExponent (domain hU hne).normalizedVolume) (hff' : f =ᵐ[(domain hU hne).normalizedVolume] f') (g : Vec d → ℝ) (hg : MeasureTheory.MemLp g p (domain hU hne).normalizedVolume) : normalizedPairing hU hne p hp_one f hf g hg = normalizedPairing hU hne p hp_one f' hf' g hg

theorem HCPolySupport.NegativeSobolev.smoothPairing_congr_ae {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (hne : U.Nonempty) (p : ENNReal) (hp_one : 1 < p) (f f' : Vec d → ℝ) (hf : MeasureTheory.MemLp f p.conjExponent (domain hU hne).normalizedVolume) (hf' : MeasureTheory.MemLp f' p.conjExponent (domain hU hne).normalizedVolume) (hff' : f =ᵐ[(domain hU hne).normalizedVolume] f') (φ : SmoothTestFunction hU) : smoothPairing hU hne p hp_one f hf φ = smoothPairing hU hne p hp_one f' hf' φ

theorem HCPolySupport.NegativeSobolev.meanZeroPairing_congr_ae {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (hne : U.Nonempty) (p : ENNReal) (hp_one : 1 < p) (f f' : Vec d → ℝ) (hf : MeasureTheory.MemLp f p.conjExponent (domain hU hne).normalizedVolume) (hf' : MeasureTheory.MemLp f' p.conjExponent (domain hU hne).normalizedVolume) (hff' : f =ᵐ[(domain hU hne).normalizedVolume] f') (φ : MeanZeroW1pTestFunction hU hne p) : meanZeroPairing hU hne p hp_one f hf φ = meanZeroPairing hU hne p hp_one f' hf' φ

theorem HCPolySupport.NegativeSobolev.smoothNegativeSobolevSeminorm_congr_ae {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (hne : U.Nonempty) (p : ENNReal) (hp_one : 1 < p) (hp_top : p ≠ ⊤) (f f' : Vec d → ℝ) (hf : MeasureTheory.MemLp f p.conjExponent (domain hU hne).normalizedVolume) (hf' : MeasureTheory.MemLp f' p.conjExponent (domain hU hne).normalizedVolume) (hff' : f =ᵐ[(domain hU hne).normalizedVolume] f') : smoothNegativeSobolevSeminorm hU hne p hp_one hp_top f hf = smoothNegativeSobolevSeminorm hU hne p hp_one hp_top f' hf'

theorem HCPolySupport.NegativeSobolev.meanZeroNegativeSobolevSeminorm_congr_ae {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (hne : U.Nonempty) (p : ENNReal) (hp_one : 1 < p) (hp_top : p ≠ ⊤) (f f' : Vec d → ℝ) (hf : MeasureTheory.MemLp f p.conjExponent (domain hU hne).normalizedVolume) (hf' : MeasureTheory.MemLp f' p.conjExponent (domain hU hne).normalizedVolume) (hff' : f =ᵐ[(domain hU hne).normalizedVolume] f') : meanZeroNegativeSobolevSeminorm hU hne p hp_one hp_top f hf = meanZeroNegativeSobolevSeminorm hU hne p hp_one hp_top f' hf'

The distinct p = 2 aliases

@[reducible, inline]

noncomputable abbrev HCPolySupport.NegativeSobolev.smoothNegativeHMinusOneSeminorm {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (hne : U.Nonempty) (f : Vec d → ℝ) (hf : MeasureTheory.MemLp f (ENNReal.conjExponent 2) (domain hU hne).normalizedVolume) : ENNReal

The normalized zero-boundary H^{-1} seminorm.

Equations

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

@[reducible, inline]

noncomputable abbrev HCPolySupport.NegativeSobolev.meanZeroNegativeHMinusOneSeminorm {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (hne : U.Nonempty) (f : Vec d → ℝ) (hf : MeasureTheory.MemLp f (ENNReal.conjExponent 2) (domain hU hne).normalizedVolume) : ENNReal

The normalized mean-zero H^{-1} seminorm.

Equations

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