Coarse-graining support: Support.Besov.Positive.ExactOverlapEuclidean

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

Exact Euclidean-valued overlapping positive-order Besov kernel

This module specializes the exact Chapter 1 overlap kernel to the source-facing fractional full norm for vector fields at p = q = 2. Both the seminorm and the root mean are aggregated over coordinates with the Euclidean ℓ² norm. All quantities remain ENNReal-valued, so no finiteness assumption is hidden in the definition.

noncomputable def HCPolySupport.exactOverlapTwoParameters (s : ↑(Set.Ioo 0 1)) : ExactOverlapFiniteParameters

The exact finite-overlap parameters with p = q = 2 and 0 < s < 1.

Equations

• HCPolySupport.exactOverlapTwoParameters s = { s := ↑s, p := 2, q := 2, admissible := ⋯ }

structure HCPolySupport.ExactOverlapEuclideanIntegrable {d : ℕ} (Q : TriadicCube d) (F : Vec d → Vec d) : Prop

Coordinatewise integrability certificates for a Euclidean-valued field. Each coordinate is certified on the root cube and on every enlarged overlap cube used by the exact scalar kernel.

• coordinate (i : Fin d) : ExactOverlapIntegrable Q fun (x : Vec d) => F x i

theorem HCPolySupport.exactOverlapEuclideanZeroIntegrable {d : ℕ} (Q : TriadicCube d) : ExactOverlapEuclideanIntegrable Q fun (x : Vec d) => 0

Canonical coordinatewise certificates for the zero vector field.

noncomputable def HCPolySupport.exactOverlapEuclideanRootMeanENorm {d : ℕ} (Q : TriadicCube d) (F : Vec d → Vec d) (hF : ExactOverlapEuclideanIntegrable Q F) : ENNReal

Euclidean magnitude of the certified coordinate root means, retained in ENNReal.

Equations

• HCPolySupport.exactOverlapEuclideanRootMeanENorm Q F hF = (∑ i : Fin d, ENNReal.ofReal |HCPolySupport.exactOverlapRootMean Q (fun (x : HCPolySupport.Vec d) => F x i) ⋯| ^ 2) ^ 2⁻¹

noncomputable def HCPolySupport.exactOverlapEuclideanSeminormTwo {d : ℕ} (s : ↑(Set.Ioo 0 1)) (Q : TriadicCube d) (F : Vec d → Vec d) (hF : ExactOverlapEuclideanIntegrable Q F) : ENNReal

Exact Euclidean-valued overlap Besov seminorm at p = q = 2, obtained by Euclidean aggregation of the exact scalar coordinate seminorms.

Equations

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

noncomputable def HCPolySupport.exactOverlapEuclideanNormTwo {d : ℕ} (s : ↑(Set.Ioo 0 1)) (Q : TriadicCube d) (F : Vec d → Vec d) (hF : ExactOverlapEuclideanIntegrable Q F) : ENNReal

The source-facing fractional full norm: the exact Euclidean p = q = 2 seminorm plus 3^(-s m) times the Euclidean magnitude of the coordinate root means.

Equations

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

theorem HCPolySupport.exactOverlapEuclideanRootMeanENorm_eq {d : ℕ} (Q : TriadicCube d) (F : Vec d → Vec d) (hF : ExactOverlapEuclideanIntegrable Q F) : exactOverlapEuclideanRootMeanENorm Q F hF = (∑ i : Fin d, ENNReal.ofReal |exactOverlapRootMean Q (fun (x : Vec d) => F x i) ⋯| ^ 2) ^ 2⁻¹

Evaluation of the Euclidean root-mean magnitude.

theorem HCPolySupport.exactOverlapEuclideanSeminormTwo_eq {d : ℕ} (s : ↑(Set.Ioo 0 1)) (Q : TriadicCube d) (F : Vec d → Vec d) (hF : ExactOverlapEuclideanIntegrable Q F) : exactOverlapEuclideanSeminormTwo s Q F hF = (∑ i : Fin d, exactOverlapFiniteSeminorm (exactOverlapTwoParameters s) Q (fun (x : Vec d) => F x i) ⋯ ^ 2) ^ 2⁻¹

Evaluation of the exact Euclidean p = q = 2 seminorm.

theorem HCPolySupport.exactOverlapEuclideanNormTwo_eq {d : ℕ} (s : ↑(Set.Ioo 0 1)) (Q : TriadicCube d) (F : Vec d → Vec d) (hF : ExactOverlapEuclideanIntegrable Q F) : exactOverlapEuclideanNormTwo s Q F hF = exactOverlapEuclideanSeminormTwo s Q F hF + exactOverlapRootWeight Q ↑s * exactOverlapEuclideanRootMeanENorm Q F hF

Evaluation of the source-facing fractional full norm.

theorem HCPolySupport.exactOverlapEuclideanRootMeanENorm_eq_ofReal_euclideanNorm {d : ℕ} (Q : TriadicCube d) (F : Vec d → Vec d) (hF : ExactOverlapEuclideanIntegrable Q F) : exactOverlapEuclideanRootMeanENorm Q F hF = ENNReal.ofReal (euclideanNorm fun (i : Fin d) => exactOverlapRootMean Q (fun (x : Vec d) => F x i) ⋯)

The coordinate formula for the root means is exactly the ENNReal embedding of their explicit Euclidean magnitude.

theorem HCPolySupport.exactOverlapEuclideanRootMean_coordinate_le {d : ℕ} (Q : TriadicCube d) (F : Vec d → Vec d) (hF : ExactOverlapEuclideanIntegrable Q F) (i : Fin d) : ENNReal.ofReal |exactOverlapRootMean Q (fun (x : Vec d) => F x i) ⋯| ≤ exactOverlapEuclideanRootMeanENorm Q F hF

Each coordinate root mean is bounded by the Euclidean root-mean magnitude.

theorem HCPolySupport.exactOverlapEuclideanSeminormTwo_coordinate_le {d : ℕ} (s : ↑(Set.Ioo 0 1)) (Q : TriadicCube d) (F : Vec d → Vec d) (hF : ExactOverlapEuclideanIntegrable Q F) (i : Fin d) : exactOverlapFiniteSeminorm (exactOverlapTwoParameters s) Q (fun (x : Vec d) => F x i) ⋯ ≤ exactOverlapEuclideanSeminormTwo s Q F hF

Each exact scalar coordinate seminorm is bounded by the exact Euclidean seminorm.

theorem HCPolySupport.exactOverlapEuclideanNormTwo_coordinate_le {d : ℕ} (s : ↑(Set.Ioo 0 1)) (Q : TriadicCube d) (F : Vec d → Vec d) (hF : ExactOverlapEuclideanIntegrable Q F) (i : Fin d) : exactOverlapFiniteNorm (exactOverlapTwoParameters s) Q (fun (x : Vec d) => F x i) ⋯ ≤ exactOverlapEuclideanNormTwo s Q F hF

Each exact scalar coordinate full norm is bounded by the source-facing Euclidean full norm.

theorem HCPolySupport.exactOverlapEuclideanRootMeanENorm_lt_top_iff {d : ℕ} (Q : TriadicCube d) (F : Vec d → Vec d) (hF : ExactOverlapEuclideanIntegrable Q F) : exactOverlapEuclideanRootMeanENorm Q F hF < ⊤ ↔ ∀ (i : Fin d), ENNReal.ofReal |exactOverlapRootMean Q (fun (x : Vec d) => F x i) ⋯| < ⊤

The Euclidean root-mean magnitude is finite exactly when all coordinate magnitudes are finite.

theorem HCPolySupport.exactOverlapEuclideanSeminormTwo_lt_top_iff {d : ℕ} (s : ↑(Set.Ioo 0 1)) (Q : TriadicCube d) (F : Vec d → Vec d) (hF : ExactOverlapEuclideanIntegrable Q F) : exactOverlapEuclideanSeminormTwo s Q F hF < ⊤ ↔ ∀ (i : Fin d), exactOverlapFiniteSeminorm (exactOverlapTwoParameters s) Q (fun (x : Vec d) => F x i) ⋯ < ⊤

The exact Euclidean seminorm is finite exactly when every exact scalar coordinate seminorm is finite.

theorem HCPolySupport.exactOverlapEuclideanRootMeanENorm_lt_top {d : ℕ} (Q : TriadicCube d) (F : Vec d → Vec d) (hF : ExactOverlapEuclideanIntegrable Q F) : exactOverlapEuclideanRootMeanENorm Q F hF < ⊤

The Euclidean root-mean magnitude is always finite because it is a finite coordinate sum of embedded real means.

theorem HCPolySupport.exactOverlapEuclideanNormTwo_lt_top_iff {d : ℕ} (s : ↑(Set.Ioo 0 1)) (Q : TriadicCube d) (F : Vec d → Vec d) (hF : ExactOverlapEuclideanIntegrable Q F) : exactOverlapEuclideanNormTwo s Q F hF < ⊤ ↔ ∀ (i : Fin d), exactOverlapFiniteSeminorm (exactOverlapTwoParameters s) Q (fun (x : Vec d) => F x i) ⋯ < ⊤

The source-facing Euclidean full norm is finite exactly when every exact scalar coordinate seminorm is finite. The root-mean term is automatically finite.

theorem HCPolySupport.exactOverlapEuclideanRootMeanENorm_congr_ae {d : ℕ} (Q : TriadicCube d) {F G : Vec d → Vec d} (hF : ExactOverlapEuclideanIntegrable Q F) (hG : ExactOverlapEuclideanIntegrable Q G) (hroot : ∀ (i : Fin d), (fun (x : Vec d) => F x i) =ᵐ[normalizedCubeMeasure Q] fun (x : Vec d) => G x i) : exactOverlapEuclideanRootMeanENorm Q F hF = exactOverlapEuclideanRootMeanENorm Q G hG

Coordinatewise a.e. equality on the root cube preserves the Euclidean root-mean magnitude.

theorem HCPolySupport.exactOverlapEuclideanSeminormTwo_congr_ae {d : ℕ} (s : ↑(Set.Ioo 0 1)) (Q : TriadicCube d) {F G : Vec d → Vec d} (hF : ExactOverlapEuclideanIntegrable Q F) (hG : ExactOverlapEuclideanIntegrable Q G) (hoverlap : ∀ (i : Fin d) (j : ℕ), ∀ S ∈ ScalarOverlap.centersAtDepth Q j, (fun (x : Vec d) => F x i) =ᵐ[ScalarOverlap.normalizedCubeMeasure S] fun (x : Vec d) => G x i) : exactOverlapEuclideanSeminormTwo s Q F hF = exactOverlapEuclideanSeminormTwo s Q G hG

Coordinatewise a.e. equality on every enlarged overlap cube preserves the exact Euclidean seminorm.

theorem HCPolySupport.exactOverlapEuclideanNormTwo_congr_ae {d : ℕ} (s : ↑(Set.Ioo 0 1)) (Q : TriadicCube d) {F G : Vec d → Vec d} (hF : ExactOverlapEuclideanIntegrable Q F) (hG : ExactOverlapEuclideanIntegrable Q G) (hroot : ∀ (i : Fin d), (fun (x : Vec d) => F x i) =ᵐ[normalizedCubeMeasure Q] fun (x : Vec d) => G x i) (hoverlap : ∀ (i : Fin d) (j : ℕ), ∀ S ∈ ScalarOverlap.centersAtDepth Q j, (fun (x : Vec d) => F x i) =ᵐ[ScalarOverlap.normalizedCubeMeasure S] fun (x : Vec d) => G x i) : exactOverlapEuclideanNormTwo s Q F hF = exactOverlapEuclideanNormTwo s Q G hG

Coordinatewise a.e. equality on the root and enlarged overlap cubes preserves the source-facing fractional full norm.

theorem HCPolySupport.exactOverlapEuclideanRootMeanENorm_zero {d : ℕ} (Q : TriadicCube d) : exactOverlapEuclideanRootMeanENorm Q (fun (x : Vec d) => 0) ⋯ = 0

The Euclidean root-mean magnitude vanishes on the zero vector field.

theorem HCPolySupport.exactOverlapEuclideanSeminormTwo_zero {d : ℕ} (s : ↑(Set.Ioo 0 1)) (Q : TriadicCube d) : exactOverlapEuclideanSeminormTwo s Q (fun (x : Vec d) => 0) ⋯ = 0

The exact Euclidean seminorm vanishes on the zero vector field.

theorem HCPolySupport.exactOverlapEuclideanNormTwo_zero {d : ℕ} (s : ↑(Set.Ioo 0 1)) (Q : TriadicCube d) : exactOverlapEuclideanNormTwo s Q (fun (x : Vec d) => 0) ⋯ = 0

The source-facing fractional full norm vanishes on the zero vector field.

theorem HCPolySupport.exactOverlapEuclideanRootMeanENorm_nonneg {d : ℕ} (Q : TriadicCube d) (F : Vec d → Vec d) (hF : ExactOverlapEuclideanIntegrable Q F) : 0 ≤ exactOverlapEuclideanRootMeanENorm Q F hF

Every exact Euclidean root-mean magnitude is nonnegative.

theorem HCPolySupport.exactOverlapEuclideanSeminormTwo_nonneg {d : ℕ} (s : ↑(Set.Ioo 0 1)) (Q : TriadicCube d) (F : Vec d → Vec d) (hF : ExactOverlapEuclideanIntegrable Q F) : 0 ≤ exactOverlapEuclideanSeminormTwo s Q F hF

Every exact Euclidean p = q = 2 seminorm is nonnegative.

theorem HCPolySupport.exactOverlapEuclideanNormTwo_nonneg {d : ℕ} (s : ↑(Set.Ioo 0 1)) (Q : TriadicCube d) (F : Vec d → Vec d) (hF : ExactOverlapEuclideanIntegrable Q F) : 0 ≤ exactOverlapEuclideanNormTwo s Q F hF

Every source-facing fractional full norm is nonnegative.