Coarse-graining support: Support.Book.Ch03.ABK26.NegativeBesov

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

ABK26 running-scale negative Besov seminorm

This file owns the literal finite-p concrete negative Besov quantity used by the Chapter 3 local coarse-graining statement. Its summation variable is the descendant depth j; the physical source scale is consequently Q.scale - j at every summand.

noncomputable def HCPolySupport.Book.Ch03.ABK26.cubeEuclideanNegativeBesovDepthEnergy {d : ℕ} (Q : TriadicCube d) (s : ↑FractionalOrder) (p : FiniteLpExponent) (F : CubeEuclideanLpField Q FiniteLpExponent.two) (j : ℕ) : ENNReal

The unrooted running-scale depth contribution to the concrete finite-p negative Besov seminorm.

Equations

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

noncomputable def HCPolySupport.Book.Ch03.ABK26.cubeEuclideanNegativeBesovESeminorm {d : ℕ} (Q : TriadicCube d) (s : ↑FractionalOrder) (p : FiniteLpExponent) (F : CubeEuclideanLpField Q FiniteLpExponent.two) : ENNReal

The source-facing concrete negative Besov seminorm. Its running-scale weight is evaluated at the descendant scale Q.scale - j, rather than frozen at the parent scale.

Equations

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

theorem HCPolySupport.Book.Ch03.ABK26.cubeEuclideanNegativeBesovESeminorm_eq_tsum_depthEnergy {d : ℕ} (Q : TriadicCube d) (s : ↑FractionalOrder) (p : FiniteLpExponent) (F : CubeEuclideanLpField Q FiniteLpExponent.two) : cubeEuclideanNegativeBesovESeminorm Q s p F = (∑' (j : ℕ), cubeEuclideanNegativeBesovDepthEnergy Q s p F j) ^ p.exponent.toReal⁻¹

Exact depth decomposition of the source-facing negative Besov seminorm.

theorem HCPolySupport.Book.Ch03.ABK26.cubeEuclideanNegativeBesovDepthEnergy_nonneg {d : ℕ} (Q : TriadicCube d) (s : ↑FractionalOrder) (p : FiniteLpExponent) (F : CubeEuclideanLpField Q FiniteLpExponent.two) (j : ℕ) : 0 ≤ cubeEuclideanNegativeBesovDepthEnergy Q s p F j

theorem HCPolySupport.Book.Ch03.ABK26.cubeEuclideanNegativeBesovESeminorm_nonneg {d : ℕ} (Q : TriadicCube d) (s : ↑FractionalOrder) (p : FiniteLpExponent) (F : CubeEuclideanLpField Q FiniteLpExponent.two) : 0 ≤ cubeEuclideanNegativeBesovESeminorm Q s p F

theorem HCPolySupport.Book.Ch03.ABK26.cubeEuclideanNegativeBesovDepthEnergy_zero {d : ℕ} (Q : TriadicCube d) (s : ↑FractionalOrder) (p : FiniteLpExponent) (F : CubeEuclideanLpField Q FiniteLpExponent.two) : cubeEuclideanNegativeBesovDepthEnergy Q s p F 0 = ENNReal.ofReal (Real.rpow 3 (↑s * p.exponent.toReal * ↑Q.scale)) * ENNReal.ofReal ‖cubeAverageVec Q F.toField‖ ^ p.exponent.toReal

theorem HCPolySupport.Book.Ch03.ABK26.cubeEuclideanNegativeBesovESeminorm_congr_ae {d : ℕ} {Q : TriadicCube d} {s : ↑FractionalOrder} {p : FiniteLpExponent} (F G : CubeEuclideanLpField Q FiniteLpExponent.two) (hFG : F.toField =ᵐ[normalizedCubeMeasure Q] G.toField) : cubeEuclideanNegativeBesovESeminorm Q s p F = cubeEuclideanNegativeBesovESeminorm Q s p G