Coarse-graining support: Support.Besov.Negative.ExactExponentBridge

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

Exponent and coefficient bridges for exact Besov duality

This module contains only arithmetic and parameter-carrier bridges. In particular, it does not compare an extended exact seminorm with a legacy real-valued wrapper.

theorem HCPolySupport.cubeBesovConjExponent_ofReal_eq_exactDualConjExponent (p : ℝ) (hp : 1 < p) : cubeBesovConjExponent (ENNReal.ofReal p) = ENNReal.ofReal (exactDualConjExponent p)

The legacy extended conjugate of a finite real exponent agrees with the real Hölder conjugate used by the exact dual kernel.

theorem HCPolySupport.cubeBesovConjExponent_exactDualConjExponent_eq_ofReal (p : ℝ) (hp : 1 < p) : cubeBesovConjExponent (ENNReal.ofReal (exactDualConjExponent p)) = ENNReal.ofReal p

Conjugating the finite exact-dual exponent recovers its source exponent.

theorem HCPolySupport.cubeBesovConjExponent_ofReal_ne_top (p : ℝ) (hp : 1 < p) : cubeBesovConjExponent (ENNReal.ofReal p) ≠ ⊤

The finite-real conjugate used by the exact dual kernel is never ∞.

theorem HCPolySupport.cubeBesovConjExponent_ofReal_one_le (p : ℝ) (hp : 1 < p) : 1 ≤ cubeBesovConjExponent (ENNReal.ofReal p)

The finite-real conjugate used by the exact dual kernel is at least one.

theorem HCPolySupport.cubeBesovConjExponent_one : cubeBesovConjExponent 1 = ⊤

The endpoint q = 1 has conjugate exponent ∞.

theorem HCPolySupport.cubeBesovConjExponent_top : cubeBesovConjExponent ⊤ = 1

The endpoint q = ∞ has conjugate exponent one.

theorem HCPolySupport.cubeBesovConjExponent_ofReal_finite (q : ℝ) (hq : 1 < q) : cubeBesovConjExponent (ENNReal.ofReal q) = ENNReal.ofReal (exactDualConjExponent q)

A finite source q > 1 has the finite real Hölder conjugate expected by the exact positive test lane.

theorem HCPolySupport.cubeBesovConjExponent_ofReal_ne_zero (p : ℝ) (hp : 1 < p) : cubeBesovConjExponent (ENNReal.ofReal p) ≠ 0

The legacy conjugate exponent is nonzero on the finite exact-dual range.

theorem HCPolySupport.exactCircLossCoefficient_le_source (d : ℕ) (s p' : ℝ) (hs : 0 ≤ s) (hp' : 1 ≤ p') : max 1 (3 ^ s) * 3 ^ (↑d / p') ≤ 3 ^ (↑d + s)

The overlap/projection loss coefficient is bounded by the Chapter 1 coefficient. All exponents are real and finite in this bridge.

theorem HCPolySupport.exactCircLossCoefficientENNReal_le_source (d : ℕ) (s p' : ℝ) (hs : 0 ≤ s) (hp' : 1 ≤ p') : ENNReal.ofReal (max 1 (3 ^ s) * 3 ^ (↑d / p')) ≤ ENNReal.ofReal (3 ^ (↑d + s))

ENNReal form of exactCircLossCoefficient_le_source, ready to multiply by an extended circ value.

theorem HCPolySupport.exactCircLossCoefficientENNReal_rpow_le_source (d : ℕ) (s p' : ℝ) (hs : 0 ≤ s) (hp' : 1 ≤ p') : max 1 (3 ^ s) * 3 ^ (↑d / p') ≤ 3 ^ (↑d + s)

Rpow-form ENNReal version of the loss bound, directly composable with an extended circ seminorm.

noncomputable def HCPolySupport.ExactDualQOneParameters.circParameters (P : ExactDualQOneParameters) : ExactCircFiniteParameters

The q = 1 dual branch supplies an admissible finite-q circ parameter with circ exponent one.

Equations

• P.circParameters = { s := P.s, p := P.p, q := 1, admissible := ⋯ }

noncomputable def HCPolySupport.ExactDualFiniteParameters.circParameters (P : ExactDualFiniteParameters) : ExactCircFiniteParameters

An interior finite dual branch supplies the matching finite circ branch.

Equations

• P.circParameters = { s := P.s, p := P.p, q := P.q, admissible := ⋯ }

noncomputable def HCPolySupport.ExactDualTopParameters.circParameters (P : ExactDualTopParameters) : ExactCircTopParameters

The q = ∞ dual branch supplies the matching top circ branch.

Equations

• P.circParameters = { s := P.s, p := P.p, admissible := ⋯ }