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

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

Additional API for the fractional Sobolev seminorm

Reuse-surface lemmas that are not needed by the W^{s,p} versus B^s_{p,p} comparison proofs themselves:

• the p = ∞ Hölder-endpoint characterization;
• swap symmetry of the unnormalized Set-variant (the kernel is odd under the pair swap, the seminorm even);
• the cube/Set relation (the ⨍∫ normalization is a volume factor at power 1/p);
• translation covariance along the triadic lattice (translateCube), via the translation pushforward of the product measure.

A.e.-congruence lemmas live in CongruenceAE.lean.

theorem HCPolySupport.Gagliardo.cubeGagliardoESeminorm_top {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (Q : TriadicCube d) (s : ℝ) (u : Vec d → E) (hu : MeasureTheory.AEStronglyMeasurable (gagliardoKernel s ⊤ u) (gagliardoCubeMeasure Q)) : cubeGagliardoESeminorm Q s ⊤ u = essSup (fun (z : Vec d × Vec d) => ‖dist z.1 z.2 ^ (-s) • (u z.1 - u z.2)‖ₑ) (gagliardoCubeMeasure Q)

At p = ∞ the fractional Sobolev seminorm is the essential Hölder C^{0,s} seminorm: the kernel exponent collapses to s and the eLpNorm becomes an essential supremum.

theorem HCPolySupport.Gagliardo.gagliardoESeminormOn_comp_swap {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (A : Set (Vec d)) (s : ℝ) (p : ENNReal) (u : Vec d → E) : MeasureTheory.eLpNorm (gagliardoKernel s p u ∘ Prod.swap) p ((MeasureTheory.volume.restrict A).prod (MeasureTheory.volume.restrict A)) = gagliardoESeminormOn A s p u

Swap symmetry of the unnormalized seminorm: precomposing the kernel with the pair swap changes nothing, since the kernel is odd under the swap and the seminorm is even.

theorem HCPolySupport.Gagliardo.cubeGagliardoESeminorm_eq_smul_gagliardoESeminormOn {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (Q : TriadicCube d) (s : ℝ) {p : ENNReal} (u : Vec d → E) : cubeGagliardoESeminorm Q s p u = ENNReal.ofReal (cubeVolume Q)⁻¹ ^ (1 / p).toReal • gagliardoESeminormOn (cubeSet Q) s p u

Relation between the cube-normalized seminorm and the unnormalized Set-variant: the manuscript's ⨍∫ normalization contributes the volume factor at power 1/p.

noncomputable def HCPolySupport.Gagliardo.cubeShiftVector {d : ℕ} (shift : Fin d → ℤ) (Q : TriadicCube d) : Vec d

The real translation vector realizing translateCube shift Q.

Equations

• HCPolySupport.Gagliardo.cubeShiftVector shift Q i = ↑(shift i) * HCPolySupport.cubeScaleFactor Q

theorem HCPolySupport.Gagliardo.cubeGagliardoESeminorm_translate {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (shift : Fin d → ℤ) (Q : TriadicCube d) (s : ℝ) {p : ENNReal} (u : Vec d → E) : cubeGagliardoESeminorm (translateCube shift Q) s p u = cubeGagliardoESeminorm Q s p fun (x : Vec d) => u (x + cubeShiftVector shift Q)

Translation covariance of the fractional Sobolev seminorm: translating the cube matches precomposing with the translation, for every exponent p.