Coarse-graining support: Support.Deterministic.HomogenizationBlackBoxes.DualityExponentLoss

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

Exponent-loss Besov bridge

This file contains the pure function-space exponent-loss bridge used by the sharp-boundary scalar duality path. It consumes the Chapter 1 legacy finite-truncation, totalized-real, disjoint/componentwise compatibility lane; it is not an exact ENNReal source-norm bridge.

noncomputable def HCPolySupport.besovExponentLossGap (s t : ℝ) : ℝ

Geometric singular factor for the embedding B^{-t}_{2,2,dual} -> B^{-s}_{2,2,circ}.

The projection-test proof has singularities both at t = 0 and at s = t. This is definitionally the coefficient proved in Chapter 1's pure Besov dual-to-circ bridge, repeated in the root namespace so deterministic theorem surfaces do not mention book-facing names.

Equations

• HCPolySupport.besovExponentLossGap s t = (1 - Real.rpow 3 (-s))⁻¹ + 2 * (1 - Real.rpow 3 (-t))⁻¹ * (1 - Real.rpow 3 (-(s - t)))⁻¹

theorem HCPolySupport.besovExponentLossGap_nonneg {s t : ℝ} (ht : 0 < t) (hts : t < s) : 0 ≤ besovExponentLossGap s t

theorem HCPolySupport.besovExponentLossGap_half_le_fiftyFive_inv_sq {s : ℝ} (hs : 0 < s) (hs_lt : s < 1) : besovExponentLossGap s (s / 2) ≤ 55 * s⁻¹ ^ 2

Half-exponent specialization of the geometric gap. This is the one-parameter loss used when the downstream theorem exposes only the larger output exponent s and measures the localized flux defect at s / 2.

theorem HCPolySupport.memVectorL2_of_isPotentialZeroTraceOn {d : ℕ} {U : Set (Vec d)} {w : Vec d → Vec d} (hw : IsPotentialZeroTraceOn U w) : MemVectorL2 U w

A zero-trace potential field has the L² membership supplied by its H¹₀ primitive. This local copy avoids importing the Ch1 public theorem layer into the deterministic black-box namespace.

noncomputable def HCPolySupport.cubeScaleNormalizedDualNegativeBesovVectorNormTwo {d : ℕ} (Q : TriadicCube d) (s : ℝ) (F : Vec d → Vec d) : ℝ

Root-namespace version of the note-normalized vector genuine dual negative Besov norm. This matches the Chapter 3 public definition but lives in the deterministic black-box layer to avoid a reverse dependency on the book-facing namespace.

Equations

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

theorem HCPolySupport.cubeScaleNormalizedDualNegativeBesovVectorNormTwo_nonneg {d : ℕ} (Q : TriadicCube d) (s : ℝ) (F : Vec d → Vec d) : 0 ≤ cubeScaleNormalizedDualNegativeBesovVectorNormTwo Q s F

noncomputable def HCPolySupport.localizedScaleNormalizedDualNegativeBesovVectorAverageTwo {d : ℕ} (Q : TriadicCube d) (s : ℝ) (F : Vec d → Vec d) (j : ℕ) : ℝ

Localized descendant ℓ² average of note-normalized vector genuine-dual negative Besov norms.

Equations

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

theorem HCPolySupport.localizedScaleNormalizedDualNegativeBesovVectorAverageTwo_nonneg {d : ℕ} (Q : TriadicCube d) (s : ℝ) (F : Vec d → Vec d) (j : ℕ) : 0 ≤ localizedScaleNormalizedDualNegativeBesovVectorAverageTwo Q s F j

theorem HCPolySupport.dualNegativeBesovNorm_le_card_mul_localizationConstant_mul_average {d : ℕ} (Q : TriadicCube d) (s : ℝ) (F : Vec d → Vec d) (j : ℕ) (hs : 0 < s) (hF : MemVectorL2 (cubeSet Q) F) : cubeScaleNormalizedDualNegativeBesovVectorNormTwo Q s F ≤ ↑(Fintype.card (Fin d)) * Book.Ch01.Legacy.negativeBesovLocalizeConstant d * localizedScaleNormalizedDualNegativeBesovVectorAverageTwo Q s F j

Componentwise Ch1 negative localization, repackaged for the deterministic note-normalized vector full-dual norm.

def HCPolySupport.ConcreteNegativeFromDualExponentLoss (d : ℕ) (C : ℝ) : Prop

Pure function-space bridge: concrete/circ negative Besov at the larger exponent s is controlled by genuine dual negative Besov at the smaller exponent t.

Equations

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

theorem HCPolySupport.concreteNegativeFromDualExponentLoss_geometric (d : ℕ) : ConcreteNegativeFromDualExponentLoss d 1

The pure Chapter 1 dual-to-circ theorem realizes the deterministic exponent-loss bridge with unit prefactor.

theorem HCPolySupport.cubeBesovNegativeVectorSeminormTwo_le_localizedDualAverage_exponentLoss {d : ℕ} (Q : TriadicCube d) (F : Vec d → Vec d) {s t : ℝ} (j : ℕ) (ht : 0 < t) (hts : t < s) (hs_lt_one : s < 1) (hF : MemVectorL2 (cubeSet Q) F) : cubeBesovNegativeVectorSeminormTwo Q s F ≤ ↑(Fintype.card (Fin d)) * Book.Ch01.Legacy.negativeBesovLocalizeConstant d * besovExponentLossGap s t * localizedScaleNormalizedDualNegativeBesovVectorAverageTwo Q t F j

Localized concrete/circ consequence of the exponent-loss bridge and Ch1 negative Besov localization.

This is the downstream-facing form: the parent concrete negative Besov seminorm is controlled by the descendant RMS of note-normalized vector full-dual norms at the lower exponent.