DepthDowngrade

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

From the ℓ^∞-over-depths multiscale Poincaré estimate to the ℓ² one

Source: ABK26 (l.Besov.grad.to.function, e.v.in.Bpps.vs.nabla.v.in.B.pp.minus.t) as consumed at e.split.besov.stuff inside the proof of l.Dh.bound.

CoarseGraining proves the function-from-gradient comparison with an ℓ^∞-over-depths left hand side, Book.Ch01.Legacy.h1_fluctuation_partialNormTop_two_le_sum_grad_circNorm:

‖ fluct u ‖_{B^{s}_{2,∞}(Q), M} ≤ C(d,Q) ∑_i [∂_i u]^{circ}_{B^{-(1-s)}_{2,1}(Q)} .

The Besov product estimate of Provider.DhBound.Besov.Product consumes instead the ℓ²-over-depths seminorm [u]_{B^{3/8}_{2,2}(Q), N}. The two are related by summing a geometric series: at any two exponents s < t,

[u]^{+}_{B^{s}_{2,2}(Q), N} ≤ (1 - 3^{-2(t-s)})^{-1/2} 3^{t·scale} ‖u‖_{B^{t}_{2,∞}(Q), N},

because the depth-j contributions at the two exponents differ exactly by the factor 3^{(s-t)j}.

The consuming instance is s = 3/8, t = 1/2; the gradient side then sits at -(1 - 1/2) = -1/2, which is downgraded to the gauge exponent -3/8 by the CoarseGraining circ comparison cubeBesovCircNorm_two_one_component_le_scaleWeight_neg_mul_gap_geometric_of_bddAbove (gap 1/2 - 3/8 = 1/8 > 0).

The depth-level extraction step (3^{-t·scale} [u]^{+}_{depth j, t} ≤ ‖u‖_{B^{t}_{2,∞}, M} for j ≤ M) exists in CoarseGraining only as a private lemma of Book/Ch01/Theorems/CutoffProduct.lean; it is re-proved here from the public cubeBesovPositiveScalarDepthSeminorm_eq_scaleWeight_neg_mul_cubeBesovDepthSeminorm_two and Finset.le_sup'.

Exponent conversion at a fixed depth

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.cubeBesovPositiveScalarDepthSeminorm_eq_gap_mul {d : ℕ} (Q : HCPolySupport.TriadicCube d) (a b : ℝ) (v : HCPolySupport.Vec d → ℝ) (j : ℕ) : HCPolySupport.cubeBesovPositiveScalarDepthSeminorm Q a v j = Real.rpow 3 ((a - b) * ↑j) * HCPolySupport.cubeBesovPositiveScalarDepthSeminorm Q b v j

Exact depthwise conversion between two positive-Besov exponents.

Depth-level extraction from the ℓ^∞ norm

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.cubeBesovPartialNormTop_nonneg {d : ℕ} (Q : HCPolySupport.TriadicCube d) (s : ℝ) (M : ℕ) (v : HCPolySupport.Vec d → ℝ) : 0 ≤ HCPolySupport.cubeBesovPartialNormTop Q s 2 M v

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.cubeBesovPositiveScalarDepthSeminorm_le_scaleWeight_neg_mul_partialNormTop {d : ℕ} (Q : HCPolySupport.TriadicCube d) (s : ℝ) (M j : ℕ) (v : HCPolySupport.Vec d → ℝ) (hj : j ∈ Finset.range (M + 1)) : HCPolySupport.cubeBesovPositiveScalarDepthSeminorm Q s v j ≤ HCPolySupport.cubeBesovScaleWeight (-s) Q * HCPolySupport.cubeBesovPartialNormTop Q s 2 M v

Depth-level extraction. Local re-proof of the CoarseGraining private lemma Book.Ch01.Legacy.cubeBesovScaleWeight_mul_positiveScalarDepthSeminorm_le_partialNormTop, in the divided form used below.

The ℓ^∞ → ℓ² downgrade

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.cubeBesovPositiveScalarPartialSeminormTwo_le_gap_geometric_mul_partialNormTop {d : ℕ} (Q : HCPolySupport.TriadicCube d) {s t : ℝ} (hst : s < t) (M : ℕ) (v : HCPolySupport.Vec d → ℝ) : HCPolySupport.cubeBesovPositiveScalarPartialSeminormTwo Q s M v ≤ √(1 - Real.rpow 3 (-2 * (t - s)))⁻¹ * (HCPolySupport.cubeBesovScaleWeight (-t) Q * HCPolySupport.cubeBesovPartialNormTop Q t 2 M v)

The ℓ^∞-to-ℓ² positive Besov downgrade. At any two exponents s < t, the finite-depth ℓ² positive seminorm at s is controlled by the finite-depth ℓ^∞ norm at t, with the geometric loss of the exponent gap.

The origin-cube consumer at the sensitivity exponents

noncomputable def Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.sensitivityGapConst : ℝ

The geometric loss of the 1/2 → 3/8 exponent gap.

Equations

• Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.sensitivityGapConst = √(1 - Real.rpow 3 (-2 * (1 / 2 - 3 / 8)))⁻¹

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.sensitivityGapConst_nonneg : 0 ≤ sensitivityGapConst

noncomputable def Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.depthDowngradeConst (d : ℕ) : ℝ

The explicit constant of the origin-cube function-from-gradient estimate at the sensitivity exponents.

Equations

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

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.cubeBesovCircNorm_half_grad_originCube_le {d : ℕ} (G : HCPolySupport.Vec d → HCPolySupport.Vec d) (i : Fin d) (hBdd : BddAbove (Set.range fun (N : ℕ) => HCPolySupport.cubeBesovNegativeVectorPartialSeminormTwo (HCPolySupport.originCube d 0) (3 / 8) N G)) : (HCPolySupport.cubeBesovCircNorm (HCPolySupport.originCube d 0) (1 / 2) 2 1 fun (x : HCPolySupport.Vec d) => G x i) ≤ sensitivityGapConst * HCPolySupport.cubeBesovNegativeVectorSeminormTwo (HCPolySupport.originCube d 0) (3 / 8) G

The componentwise circ norm of the gradient, at the exponent produced by the multiscale Poincaré estimate, is controlled by the gauge-exponent negative seminorm of the full gradient.

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.cubeBesovPositiveScalarPartialSeminormTwo_h1_originCube_le {d : ℕ} (M : ℕ) (u : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d 0))) (hBdd : BddAbove (Set.range fun (N : ℕ) => HCPolySupport.cubeBesovNegativeVectorPartialSeminormTwo (HCPolySupport.originCube d 0) (3 / 8) N fun (x : HCPolySupport.Vec d) => u.grad x)) : (HCPolySupport.cubeBesovPositiveScalarPartialSeminormTwo (HCPolySupport.originCube d 0) (3 / 8) M fun (x : HCPolySupport.Vec d) => u.toFun x) ≤ depthDowngradeConst d * HCPolySupport.cubeBesovNegativeVectorSeminormTwo (HCPolySupport.originCube d 0) (3 / 8) fun (x : HCPolySupport.Vec d) => u.grad x

The origin-cube function-from-gradient estimate in the ℓ² form.