Documentation

LeanPool.HighContrastHomogenization.Support.Sobolev.Fractional.CongruenceAE

Coarse-graining support: Support.Sobolev.Fractional.CongruenceAE #

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

Almost-everywhere congruence for the fractional Sobolev and Besov seminorms #

All quantities in the W^{s,p} versus B^s_{p,p} comparison are invariant under modifying u on a null set of the cube. This file proves the congruence lemmas once, against the canonical hypothesis u =ᵐ[cubeMeasure Q] v:

These discharge the congr_ae item of the frozen API surface and enable the measurability-free public wrapper of CG Lemma 1.3.

source
theorem HCPolySupport.Gagliardo.ae_normalizedCubeMeasure_iff {d : ℕ} {Q : TriadicCube d} {prop : Vec d → Prop} :
(∀ᵐ (x : Vec d) ∂normalizedCubeMeasure Q, prop x) ↔ ∀ᵐ (x : Vec d) ∂cubeMeasure Q, prop x

The normalized and plain cube measures have the same ae filter.

source
theorem HCPolySupport.Gagliardo.gagliardoKernel_congr_ae {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {Q : TriadicCube d} {s : ℝ} {p : ENNReal} {u v : Vec d → E} (h : u =ᵐ[cubeMeasure Q] v) :
gagliardoKernel s p u =ᵐ[gagliardoCubeMeasure Q] gagliardoKernel s p v

Kernel congruence: modifying u on a cube-null set changes the Gagliardo kernel only on a gagliardoCubeMeasure-null set of pairs.

source
theorem HCPolySupport.Gagliardo.cubeGagliardoESeminorm_congr_ae {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {Q : TriadicCube d} {s : ℝ} {p : ENNReal} {u v : Vec d → E} (h : u =ᵐ[cubeMeasure Q] v) :
cubeGagliardoESeminorm Q s p u = cubeGagliardoESeminorm Q s p v

A.e.-congruence of the fractional Sobolev seminorm.

source
theorem HCPolySupport.Gagliardo.memWsp_congr_ae {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {Q : TriadicCube d} {s : ℝ} {p : ENNReal} {u v : Vec d → E} (h : u =ᵐ[cubeMeasure Q] v) :
MemWsp Q s p u ↔ MemWsp Q s p v

A.e.-congruence of W^{s,p} membership.

source
theorem HCPolySupport.Gagliardo.ae_overlap_of_ae_cube {d : ℕ} {Q : TriadicCube d} {u v : Vec d → ℝ} {j : ℕ} {S : TriadicCube d} (hS : S ∈ ScalarOverlap.centersAtDepth Q j) (h : u =ᵐ[cubeMeasure Q] v) :
u =ᵐ[MeasureTheory.volume.restrict (ScalarOverlap.cubeSet S)] v

Restriction of the congruence hypothesis to an overlap center's enlarged cube.

source
theorem HCPolySupport.Gagliardo.overlap_cubeAverage_congr_ae {d : ℕ} {Q : TriadicCube d} {u v : Vec d → ℝ} {j : ℕ} {S : TriadicCube d} (hS : S ∈ ScalarOverlap.centersAtDepth Q j) (h : u =ᵐ[cubeMeasure Q] v) :
ScalarOverlap.cubeAverage S u = ScalarOverlap.cubeAverage S v
source
theorem HCPolySupport.Gagliardo.overlap_oscillation_congr_ae {d : ℕ} {Q : TriadicCube d} {u v : Vec d → ℝ} {p : ENNReal} {j : ℕ} {S : TriadicCube d} (hS : S ∈ ScalarOverlap.centersAtDepth Q j) (h : u =ᵐ[cubeMeasure Q] v) :
cubeBesovOverlapOscillation S p u = cubeBesovOverlapOscillation S p v
source
theorem HCPolySupport.Gagliardo.overlap_depthAverage_congr_ae {d : ℕ} {Q : TriadicCube d} {u v : Vec d → ℝ} {p : ENNReal} {j : ℕ} (h : u =ᵐ[cubeMeasure Q] v) :
cubeBesovOverlapDepthAverage Q p u j = cubeBesovOverlapDepthAverage Q p v j
source
theorem HCPolySupport.Gagliardo.overlap_partialSeminorm_congr_ae {d : ℕ} {Q : TriadicCube d} {u v : Vec d → ℝ} {s : ℝ} {p q : ENNReal} {N : ℕ} (h : u =ᵐ[cubeMeasure Q] v) :
cubeBesovOverlapPartialSeminorm Q s p q N u = cubeBesovOverlapPartialSeminorm Q s p q N v
source
theorem HCPolySupport.Gagliardo.cubeBesovOverlapSeminorm_congr_ae {d : ℕ} {Q : TriadicCube d} {u v : Vec d → ℝ} {s : ℝ} {p q : ENNReal} (h : u =ᵐ[cubeMeasure Q] v) :
cubeBesovOverlapSeminorm Q s p q u = cubeBesovOverlapSeminorm Q s p q v

A.e.-congruence of the full overlapping Besov seminorm (any q).