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

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

Generic normalized W^{1,p} implementation kernel

This module implements normalized W^{1,p} quantities on an arbitrary positive-finite-volume BoundedMeasurableDomain. It is a reusable analytic kernel, not the Chapter 1 source-facing carrier: Chapter 1 exposes these operations only after restricting to its nonempty bounded open convex-domain facade.

theorem HCPolySupport.W1pFunction.gradEuclideanMemLp {d : ℕ} (U : BoundedMeasurableDomain d) (p : ENNReal) (u : W1pFunction (↑U) p) : MeasureTheory.MemLp (fun (x : Vec d) => euclideanNorm (u.grad x)) p U.normalizedVolume

Componentwise L^p control of a weak gradient gives L^p control of its explicit Euclidean magnitude, after volume normalization.

noncomputable def HCPolySupport.BoundedMeasurableDomain.volumeReal {d : ℕ} (U : BoundedMeasurableDomain d) : ℝ

The real Lebesgue volume of a bounded measurable domain. Its conversion from ℝ≥0∞ is certified by volume_ne_top.

Equations

• U.volumeReal = (MeasureTheory.volume ↑U).toReal

theorem HCPolySupport.BoundedMeasurableDomain.volumeReal_pos {d : ℕ} (U : BoundedMeasurableDomain d) : 0 < U.volumeReal

A bounded measurable domain has strictly positive real Lebesgue volume.

theorem HCPolySupport.BoundedMeasurableDomain.volumeReal_ne_zero {d : ℕ} (U : BoundedMeasurableDomain d) : U.volumeReal ≠ 0

Generic kernel

The declarations below are deliberately nested under BoundedMeasurableDomain.NormalizedW1pKernel. They require only the broad bounded-measurable positive-volume carrier and must not be presented as the Chapter 1 source-facing domain API.

noncomputable def HCPolySupport.BoundedMeasurableDomain.NormalizedW1pKernel.seminorm {d : ℕ} (U : BoundedMeasurableDomain d) (p : ENNReal) (_hp_one : 1 ≤ p) (_hp_top : p ≠ ⊤) (u : W1pFunction (↑U) p) : ℝ

The finite-exponent normalized W^{1,p} seminorm in the generic kernel.

Equations

• HCPolySupport.BoundedMeasurableDomain.NormalizedW1pKernel.seminorm U p _hp_one _hp_top u = U.normalizedEuclideanLpNorm p u.grad ⋯

theorem HCPolySupport.BoundedMeasurableDomain.NormalizedW1pKernel.seminorm_eq {d : ℕ} (U : BoundedMeasurableDomain d) (p : ENNReal) (hp_one : 1 ≤ p) (hp_top : p ≠ ⊤) (u : W1pFunction (↑U) p) : seminorm U p hp_one hp_top u = U.normalizedEuclideanLpNorm p u.grad ⋯

Characterization of the generic finite-exponent normalized seminorm.

theorem HCPolySupport.BoundedMeasurableDomain.NormalizedW1pKernel.seminorm_congr_ae {d : ℕ} (U : BoundedMeasurableDomain d) (p : ENNReal) (hp_one : 1 ≤ p) (hp_top : p ≠ ⊤) (u v : W1pFunction (↑U) p) (hgrad : u.grad =ᵐ[U.normalizedVolume] v.grad) : seminorm U p hp_one hp_top u = seminorm U p hp_one hp_top v

The generic finite-exponent seminorm is invariant under an a.e. equality of the explicitly stored weak gradients.

noncomputable def HCPolySupport.BoundedMeasurableDomain.NormalizedW1pKernel.norm {d : ℕ} (U : BoundedMeasurableDomain d) (p : ENNReal) (hp_one : 1 ≤ p) (hp_top : p ≠ ⊤) (u : W1pFunction (↑U) p) : ℝ

The generic finite-exponent normalized W^{1,p} norm: (‖∇u‖^p + |U|^(-p/d) ‖u‖^p)^(1/p).

Equations

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

theorem HCPolySupport.BoundedMeasurableDomain.NormalizedW1pKernel.norm_eq {d : ℕ} (U : BoundedMeasurableDomain d) (p : ENNReal) (hp_one : 1 ≤ p) (hp_top : p ≠ ⊤) (u : W1pFunction (↑U) p) : norm U p hp_one hp_top u = (seminorm U p hp_one hp_top u ^ p.toReal + U.volumeReal ^ (-(p.toReal / ↑d)) * U.normalizedLpNorm p u.toFun ⋯ ^ p.toReal) ^ p.toReal⁻¹

Characterization of the generic finite-exponent normalized norm.

theorem HCPolySupport.BoundedMeasurableDomain.NormalizedW1pKernel.norm_congr_ae {d : ℕ} (U : BoundedMeasurableDomain d) (p : ENNReal) (hp_one : 1 ≤ p) (hp_top : p ≠ ⊤) (u v : W1pFunction (↑U) p) (hfun : u.toFun =ᵐ[U.normalizedVolume] v.toFun) (hgrad : u.grad =ᵐ[U.normalizedVolume] v.grad) : norm U p hp_one hp_top u = norm U p hp_one hp_top v

The generic finite-exponent normalized norm is invariant under separate a.e. equalities of the function and its explicitly stored weak gradient.

noncomputable def HCPolySupport.BoundedMeasurableDomain.NormalizedW1pKernel.seminormTop {d : ℕ} (U : BoundedMeasurableDomain d) (u : W1pFunction ↑U ⊤) : ℝ

The generic normalized W^{1,∞} seminorm of a weak Sobolev witness.

Equations

• HCPolySupport.BoundedMeasurableDomain.NormalizedW1pKernel.seminormTop U u = U.normalizedEuclideanLpNorm ⊤ u.grad ⋯

theorem HCPolySupport.BoundedMeasurableDomain.NormalizedW1pKernel.seminormTop_eq {d : ℕ} (U : BoundedMeasurableDomain d) (u : W1pFunction ↑U ⊤) : seminormTop U u = U.normalizedEuclideanLpNorm ⊤ u.grad ⋯

Characterization of the generic normalized W^{1,∞} seminorm.

theorem HCPolySupport.BoundedMeasurableDomain.NormalizedW1pKernel.seminormTop_congr_ae {d : ℕ} (U : BoundedMeasurableDomain d) (u v : W1pFunction ↑U ⊤) (hgrad : u.grad =ᵐ[U.normalizedVolume] v.grad) : seminormTop U u = seminormTop U v

The generic endpoint seminorm is invariant under an a.e. equality of the explicitly stored weak gradients.

noncomputable def HCPolySupport.BoundedMeasurableDomain.NormalizedW1pKernel.normTop {d : ℕ} (U : BoundedMeasurableDomain d) (u : W1pFunction ↑U ⊤) : ℝ

The generic endpoint normalized W^{1,∞} norm. The two terms are added, rather than combined using a maximum.

Equations

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

theorem HCPolySupport.BoundedMeasurableDomain.NormalizedW1pKernel.normTop_eq {d : ℕ} (U : BoundedMeasurableDomain d) (u : W1pFunction ↑U ⊤) : normTop U u = seminormTop U u + U.volumeReal ^ (-(1 / ↑d)) * U.normalizedLpNorm ⊤ u.toFun ⋯

Characterization of the generic endpoint normalized norm.

theorem HCPolySupport.BoundedMeasurableDomain.NormalizedW1pKernel.normTop_congr_ae {d : ℕ} (U : BoundedMeasurableDomain d) (u v : W1pFunction ↑U ⊤) (hfun : u.toFun =ᵐ[U.normalizedVolume] v.toFun) (hgrad : u.grad =ᵐ[U.normalizedVolume] v.grad) : normTop U u = normTop U v

The generic endpoint normalized norm is invariant under separate a.e. equalities of the function and its explicitly stored weak gradient.