Coarse-graining support: Support.Book.Ch01.Theorems.DualToCircLoss.FiniteLoss

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

Dual-to-circ finite loss

Legacy finite-truncation loss estimates for the totalized-real, disjoint/componentwise compatibility lane. They are not the exact ENNReal overlap/dual/circ kernels.

noncomputable def HCPolySupport.Book.Ch01.Legacy.dualToCircFiniteLossCoefficient (s t : ℝ) (N : ℕ) : ℝ

Finite-depth coefficient in the lossy true-dual-to-circ comparison. The outer j sum is the negative Besov scale sum, and the inner k sum is the positive test norm of the depth-j projection.

Equations

• HCPolySupport.Book.Ch01.Legacy.dualToCircFiniteLossCoefficient s t N = ∑ j ∈ Finset.range (N + 1), Real.rpow 3 (-s * ↑j) * (1 + ∑ k ∈ Finset.range j, 2 * Real.rpow 3 (t * ↑k))

theorem HCPolySupport.Book.Ch01.Legacy.dualToCircFiniteLossCoefficient_nonneg (s t : ℝ) (N : ℕ) : 0 ≤ dualToCircFiniteLossCoefficient s t N

noncomputable def HCPolySupport.Book.Ch01.Legacy.dualToCircGeometricLossCoefficient (s t : ℝ) : ℝ

Explicit geometric coefficient bounding the finite loss coefficients when 0 < t < s.

Equations

• HCPolySupport.Book.Ch01.Legacy.dualToCircGeometricLossCoefficient s t = (1 - Real.rpow 3 (-s))⁻¹ + 2 * (1 - Real.rpow 3 (-t))⁻¹ * (1 - Real.rpow 3 (-(s - t)))⁻¹

theorem HCPolySupport.Book.Ch01.Legacy.dualToCircFiniteLossCoefficient_le_geometric {s t : ℝ} (_hs : 0 < s) (ht : 0 < t) (hst : t < s) (N : ℕ) : dualToCircFiniteLossCoefficient s t N ≤ dualToCircGeometricLossCoefficient s t

theorem HCPolySupport.Book.Ch01.Legacy.dualToCircGeometricLossCoefficient_half_le_fiftyFive_inv_sq {s : ℝ} (hs : 0 < s) (hs_le : s ≤ 1) : dualToCircGeometricLossCoefficient s (s / 2) ≤ 55 * s⁻¹ ^ 2

Half-exponent geometric loss with a simple note-style s^{-2} bound.

theorem HCPolySupport.Book.Ch01.Legacy.dualToCircFiniteLossCoefficient_half_le_fiftyFive_inv_sq {s : ℝ} (hs : 0 < s) (hs_le : s ≤ 1) (N : ℕ) : dualToCircFiniteLossCoefficient s (s / 2) N ≤ 55 * s⁻¹ ^ 2

Half-exponent finite loss coefficient bounded by the explicit 55 * s^{-2} note-style loss.

noncomputable def HCPolySupport.Book.Ch01.Legacy.normalizedDualNegativeBesovVectorNormTwo {d : ℕ} (Q : Cube d) (s : ℝ) (F : Vec d → Vec d) : ℝ

Componentwise vector-valued genuine dual negative Besov norm, normalized by the parent cube scale, in the legacy totalized-real compatibility lane. This is distinct from the exact ENNReal overlap/dual/circ kernels.

Equations

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

theorem HCPolySupport.Book.Ch01.Legacy.normalizedDualNegativeBesovVectorNormTwo_nonneg {d : ℕ} (Q : Cube d) (s : ℝ) (F : Vec d → Vec d) : 0 ≤ normalizedDualNegativeBesovVectorNormTwo Q s F

theorem HCPolySupport.Book.Ch01.Legacy.component_memLp_normalizedCubeMeasure_of_memVectorL2_cubeSet_ch1 {d : ℕ} (Q : Cube d) {F : Vec d → Vec d} (hF : MemVectorL2 (cubeSet Q) F) (i : Fin d) : MeasureTheory.MemLp (fun (x : Vec d) => F x i) 2 (normalizedCubeMeasure Q)

theorem HCPolySupport.Book.Ch01.Legacy.cubeBesovNegativeVectorPartialSeminormTwo_le_dualToCircFiniteLossCoefficient_mul_normalizedDual {d : ℕ} (Q : Cube d) (F : Vec d → Vec d) {s t : ℝ} (N : ℕ) (ht : 0 < t) (hF : ∀ (i : Fin d), MeasureTheory.MemLp (fun (x : Vec d) => F x i) 2 (normalizedCubeMeasure Q)) : cubeBesovNegativeVectorPartialSeminormTwo Q s N F ≤ dualToCircFiniteLossCoefficient s t N * normalizedDualNegativeBesovVectorNormTwo Q t F

theorem HCPolySupport.Book.Ch01.Legacy.cubeBesovNegativeVectorSeminormTwo_le_dualToCircCoefficientBound_mul_normalizedDual {d : ℕ} (Q : Cube d) (F : Vec d → Vec d) {s t C : ℝ} (ht : 0 < t) (hF : ∀ (i : Fin d), MeasureTheory.MemLp (fun (x : Vec d) => F x i) 2 (normalizedCubeMeasure Q)) (hcoeff : ∀ (N : ℕ), dualToCircFiniteLossCoefficient s t N ≤ C) : cubeBesovNegativeVectorSeminormTwo Q s F ≤ C * normalizedDualNegativeBesovVectorNormTwo Q t F

Full-seminorm form of the proved scale-by-scale true-dual-to-circ comparison, parametrized by any uniform bound on the finite loss coefficient.

The remaining scalar analytic work is to supply such a coefficient bound, for example with t = s / 2, where the notes lose a power of s⁻¹.

theorem HCPolySupport.Book.Ch01.Legacy.negativeBesovVectorSeminorm_le_geometricLoss_mul_normalizedDual {d : ℕ} (Q : Cube d) (F : Vec d → Vec d) {s t : ℝ} (hs : 0 < s) (ht : 0 < t) (hst : t < s) (hF : ∀ (i : Fin d), MeasureTheory.MemLp (fun (x : Vec d) => F x i) 2 (normalizedCubeMeasure Q)) : cubeBesovNegativeVectorSeminormTwo Q s F ≤ dualToCircGeometricLossCoefficient s t * normalizedDualNegativeBesovVectorNormTwo Q t F

Full finite-energy reverse comparison with the explicit geometric loss coefficient.

theorem HCPolySupport.Book.Ch01.Legacy.cubeBesovNegativeVectorSeminormTwo_le_halfDual_fiftyFive_inv_sq {d : ℕ} (Q : Cube d) (F : Vec d → Vec d) {s : ℝ} (hs : 0 < s) (hs_lt : s < 1) (hF : ∀ (i : Fin d), MeasureTheory.MemLp (fun (x : Vec d) => F x i) 2 (normalizedCubeMeasure Q)) : cubeBesovNegativeVectorSeminormTwo Q s F ≤ 55 * s⁻¹ ^ 2 * normalizedDualNegativeBesovVectorNormTwo Q (s / 2) F

Full finite-energy half-exponent reverse comparison with the explicit 55 * s^{-2} loss.

theorem HCPolySupport.Book.Ch01.Legacy.cubeBesovNegativeVectorSeminormTwo_le_halfDual_fiftyFive_inv_sq_of_memVectorL2 {d : ℕ} (Q : Cube d) (F : Vec d → Vec d) {s : ℝ} (hs : 0 < s) (hs_lt : s < 1) (hF : MemVectorL2 (cubeSet Q) F) : cubeBesovNegativeVectorSeminormTwo Q s F ≤ 55 * s⁻¹ ^ 2 * normalizedDualNegativeBesovVectorNormTwo Q (s / 2) F

Finite-energy half-exponent reverse comparison for fields supplied as L² vector fields on the cube.