Coarse-graining support: Support.Sobolev.Fractional.Definitions

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

Fractional Sobolev (Gagliardo) seminorms on triadic cubes

This file defines the volume-normalized fractional Sobolev seminorm [u]_{W_underlined^{s,p}(□)} of the manuscript (CG Chapter 1, "Fractional Sobolev seminorms") as an eLpNorm of a difference-quotient kernel over a product measure, together with the membership predicate MemWsp playing the role of u ∈ W^{s,p}(□).

Design notes:

• The kernel uses the ambient Vec d sup-norm distance, which differs from the manuscript's Euclidean distance by a factor absorbed into dimensional constants (uniformly in s, p, since the kernel exponent s + d/p is at most d + 1 on the manuscript range s < 1 ≤ p).
• The manuscript's ⨍∫ normalization is carried by the product measure gagliardoCubeMeasure (normalized in the first slot, plain in the second), not by an ad-hoc volume prefactor.
• At p = ∞ the kernel exponent s + d / p.toReal collapses to s (junk-value d / 0 = 0), so the seminorm degenerates to the essential Hölder C^{0,s} seminorm, matching the manuscript's [·]_{C^{0,s}} ≈ [·]_{W_underlined^{s,∞}} convention.
• Consumers must not unfold the definitions: the lemmas in the Internal namespace are reserved for the comparison proof files. Everything else goes through the exported API.

noncomputable def HCPolySupport.Gagliardo.kernelExponent (d : ℕ) (s : ℝ) (p : ENNReal) : ℝ

The kernel exponent s + d/p. At p = ∞ it collapses to s.

Equations

• HCPolySupport.Gagliardo.kernelExponent d s p = s + ↑d / p.toReal

theorem HCPolySupport.Gagliardo.kernelExponent_top (d : ℕ) (s : ℝ) : kernelExponent d s ⊤ = s

noncomputable def HCPolySupport.Gagliardo.gagliardoKernel {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (s : ℝ) (p : ENNReal) (u : Vec d → E) : Vec d × Vec d → E

Difference-quotient kernel of the fractional Sobolev seminorm.

Equations

• HCPolySupport.Gagliardo.gagliardoKernel s p u z = dist z.1 z.2 ^ (-HCPolySupport.Gagliardo.kernelExponent d s p) • (u z.1 - u z.2)

theorem HCPolySupport.Gagliardo.gagliardoKernel_apply {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (s : ℝ) (p : ENNReal) (u : Vec d → E) (z : Vec d × Vec d) : gagliardoKernel s p u z = dist z.1 z.2 ^ (-kernelExponent d s p) • (u z.1 - u z.2)

theorem HCPolySupport.Gagliardo.gagliardoKernel_zero {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (s : ℝ) (p : ENNReal) : gagliardoKernel s p 0 = 0

theorem HCPolySupport.Gagliardo.gagliardoKernel_add {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (s : ℝ) (p : ENNReal) (u v : Vec d → E) : gagliardoKernel s p (u + v) = gagliardoKernel s p u + gagliardoKernel s p v

theorem HCPolySupport.Gagliardo.gagliardoKernel_neg {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (s : ℝ) (p : ENNReal) (u : Vec d → E) : gagliardoKernel s p (-u) = -gagliardoKernel s p u

theorem HCPolySupport.Gagliardo.gagliardoKernel_smul {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (s : ℝ) (p : ENNReal) (c : ℝ) (u : Vec d → E) : gagliardoKernel s p (c • u) = c • gagliardoKernel s p u

noncomputable def HCPolySupport.Gagliardo.gagliardoCubeMeasure {d : ℕ} (Q : TriadicCube d) : MeasureTheory.Measure (Vec d × Vec d)

The manuscript's ⨍_□ ∫_□ normalization as a product measure: normalized in the first variable, plain restricted volume in the second.

Equations

• HCPolySupport.Gagliardo.gagliardoCubeMeasure Q = (HCPolySupport.normalizedCubeMeasure Q).prod (HCPolySupport.cubeMeasure Q)

instance HCPolySupport.Gagliardo.instIsFiniteMeasureGagliardoCubeMeasure {d : ℕ} (Q : TriadicCube d) : MeasureTheory.IsFiniteMeasure (gagliardoCubeMeasure Q)

instance HCPolySupport.Gagliardo.instSFiniteGagliardoCubeMeasure {d : ℕ} (Q : TriadicCube d) : MeasureTheory.SFinite (gagliardoCubeMeasure Q)

noncomputable def HCPolySupport.Gagliardo.cubeGagliardoESeminorm {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (Q : TriadicCube d) (s : ℝ) (p : ENNReal) (u : Vec d → E) : ENNReal

[u]_{W_underlined^{s,p}(Q)}, ℝ≥0∞-valued, defined for all p ∈ [1,∞] (p = ∞ gives the essential Hölder seminorm).

Equations

• HCPolySupport.Gagliardo.cubeGagliardoESeminorm Q s p u = MeasureTheory.eLpNorm (HCPolySupport.Gagliardo.gagliardoKernel s p u) p (HCPolySupport.Gagliardo.gagliardoCubeMeasure Q)

noncomputable def HCPolySupport.Gagliardo.cubeGagliardoSeminorm {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (Q : TriadicCube d) (s : ℝ) (p : ENNReal) (u : Vec d → E) : ℝ

Real-valued fractional Sobolev seminorm (junk value 0 when infinite).

Equations

• HCPolySupport.Gagliardo.cubeGagliardoSeminorm Q s p u = (HCPolySupport.Gagliardo.cubeGagliardoESeminorm Q s p u).toReal

noncomputable def HCPolySupport.Gagliardo.gagliardoESeminormOn {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (A : Set (Vec d)) (s : ℝ) (p : ENNReal) (u : Vec d → E) : ENNReal

Unnormalized fractional Sobolev seminorm over an arbitrary set.

Equations

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

def HCPolySupport.Gagliardo.MemWsp {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (Q : TriadicCube d) (s : ℝ) (p : ENNReal) (u : Vec d → E) : Prop

u ∈ W^{s,p}(Q): the membership predicate, mirroring MemLp.

Equations

• HCPolySupport.Gagliardo.MemWsp Q s p u = MeasureTheory.MemLp (HCPolySupport.Gagliardo.gagliardoKernel s p u) p (HCPolySupport.Gagliardo.gagliardoCubeMeasure Q)

theorem HCPolySupport.Gagliardo.Internal.cubeGagliardoESeminorm_def {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (Q : TriadicCube d) (s : ℝ) (p : ENNReal) (u : Vec d → E) : cubeGagliardoESeminorm Q s p u = MeasureTheory.eLpNorm (gagliardoKernel s p u) p (gagliardoCubeMeasure Q)

Unfolding lemma, reserved for the comparison proof files.

theorem HCPolySupport.Gagliardo.Internal.cubeGagliardoESeminorm_eq_lintegral {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {Q : TriadicCube d} {s : ℝ} {p : ENNReal} {u : Vec d → E} (hp0 : p ≠ 0) (hpt : p ≠ ⊤) (hu : MeasureTheory.AEStronglyMeasurable (gagliardoKernel s p u) (gagliardoCubeMeasure Q)) : cubeGagliardoESeminorm Q s p u = (∫⁻ (z : Vec d × Vec d), ‖gagliardoKernel s p u z‖ₑ ^ p.toReal ∂gagliardoCubeMeasure Q) ^ (1 / p.toReal)

Finite-p lintegral form, reserved for the comparison proof files.

theorem HCPolySupport.Gagliardo.MemWsp.aestronglyMeasurable {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {Q : TriadicCube d} {s : ℝ} {p : ENNReal} {u : Vec d → E} (h : MemWsp Q s p u) : MeasureTheory.AEStronglyMeasurable (gagliardoKernel s p u) (gagliardoCubeMeasure Q)

theorem HCPolySupport.Gagliardo.MemWsp.eSeminorm_lt_top {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {Q : TriadicCube d} {s : ℝ} {p : ENNReal} {u : Vec d → E} (h : MemWsp Q s p u) : cubeGagliardoESeminorm Q s p u < ⊤

theorem HCPolySupport.Gagliardo.memWsp_iff {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {Q : TriadicCube d} {s : ℝ} {p : ENNReal} {u : Vec d → E} : MemWsp Q s p u ↔ MeasureTheory.AEStronglyMeasurable (gagliardoKernel s p u) (gagliardoCubeMeasure Q) ∧ cubeGagliardoESeminorm Q s p u < ⊤

theorem HCPolySupport.Gagliardo.MemWsp.add {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {Q : TriadicCube d} {s : ℝ} {p : ENNReal} {u v : Vec d → E} (hu : MemWsp Q s p u) (hv : MemWsp Q s p v) : MemWsp Q s p (u + v)

theorem HCPolySupport.Gagliardo.MemWsp.neg {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {Q : TriadicCube d} {s : ℝ} {p : ENNReal} {u : Vec d → E} (hu : MemWsp Q s p u) : MemWsp Q s p (-u)

theorem HCPolySupport.Gagliardo.MemWsp.smul {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {Q : TriadicCube d} {s : ℝ} {p : ENNReal} {u : Vec d → E} (c : ℝ) (hu : MemWsp Q s p u) : MemWsp Q s p (c • u)

theorem HCPolySupport.Gagliardo.cubeGagliardoESeminorm_zero {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (Q : TriadicCube d) (s : ℝ) (p : ENNReal) : cubeGagliardoESeminorm Q s p 0 = 0

theorem HCPolySupport.Gagliardo.cubeGagliardoESeminorm_neg {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (Q : TriadicCube d) (s : ℝ) (p : ENNReal) (u : Vec d → E) : cubeGagliardoESeminorm Q s p (-u) = cubeGagliardoESeminorm Q s p u

theorem HCPolySupport.Gagliardo.cubeGagliardoESeminorm_const_smul {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (Q : TriadicCube d) (s : ℝ) (p : ENNReal) (c : ℝ) (u : Vec d → E) : cubeGagliardoESeminorm Q s p (c • u) = ‖c‖ₑ * cubeGagliardoESeminorm Q s p u

theorem HCPolySupport.Gagliardo.cubeGagliardoESeminorm_add_le {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {Q : TriadicCube d} {s : ℝ} {p : ENNReal} {u v : Vec d → E} (hp : 1 ≤ p) : cubeGagliardoESeminorm Q s p (u + v) ≤ cubeGagliardoESeminorm Q s p u + cubeGagliardoESeminorm Q s p v

Triangle inequality for the fractional Sobolev seminorm.

theorem HCPolySupport.Gagliardo.cubeGagliardoSeminorm_nonneg {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (Q : TriadicCube d) (s : ℝ) (p : ENNReal) (u : Vec d → E) : 0 ≤ cubeGagliardoSeminorm Q s p u