SimplexResponseBound

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

The crude response bounds at the manuscript's simplex carrier

All three steps are carried out (the decomposition itself is SimplexDissection.lean), so ABK26's application of the crude response bounds/6348 at square = spx a simplex is available at the printed carrier, with an explicit constant.

The estimate

Let T be a Kuhn cell (e.simplex.def) whose support cube is a triadic descendant of Q at scale k, and let {R_i} be the triadic Whitney dissection of the open simplex. Then

J(T, p, 0; a) <= C(d,s) . 3^{2 s (Q.scale - k)} . Lambda_{s,q}(Q; a) . |p|^2 ,
J(T, 0, q; a) <= C(d,s) . 3^{2 s (Q.scale - k)} . lambda^{-1}_{s,q}(Q; a) . |q|^2 ,

with the explicit d- and s-only constant

C(d,s) = simplexCrudeConst d s = 6 d (d+1) / (1 - 3^{2s-1}) ,

finite exactly on the window s < 1/2; at the manuscript's s = 1/4 it is 6 d (d+1) / (1 - 3^{-1/2}) < 15 d (d+1).

The boundary estimate

The identified route describes the second ingredient as a boundary count. What is proved here is the equivalent convex-collar estimate, which needs no enumeration of the d+1 faces of the simplex:

• the open simplex U contains an explicit sup-ball B(c, rho) with rho = 3^{scale} / (2(d+1)) (ball_simplexIncenter_subset_openCarrier);
• hence for 0 < lam <= 1 every point of the homothetic copy c + (1-lam)(U - c) has its whole lam rho-ball inside U (ball_subset_of_mem_shrinkToward), and that copy has volume (1-lam)^d |U|;
• a selected cube at depth t has a triadic parent that meets the complement of U and has diameter 3 . 3^{scale-t}, so the cube misses the homothetic copy at lam = 12 (d+1) 3^{-t};
• the selected cubes at depth t being disjoint, their total volume is at most (1 - (1-lam)^d) |U| <= d lam |U| = 12 d (d+1) 3^{-t} |U| (sum_cubeVolume_simplexDissection_le).

Summing the weights gives sum_i (|R_i|/|T|) 3^{2 s t_i} <= 12 d (d+1) / (1 - 3^{2s-1}) (tsum_cubeVolume_weight_le), convergent exactly on that window.

Main results

• responseJ_simplexDomain_zero_flux_le_LambdaSq, responseJ_simplexDomain_zero_slope_le_lambdaSq_inv — the crude response bounds at the simplex carrier, for 0 < s < 1/2 and any admissible exponent.

References

• ABK26, p.bfA.multiscalebound, Step 1, l.subadd.betterer, e.simplex.def.

Homothetic shrinking of a convex set

def Algsuperdiff.Section3.Provider.Multiscale.shrinkToward {d : ℕ} (c : HCPolySupport.Vec d) (lam : ℝ) (U : Set (HCPolySupport.Vec d)) : Set (HCPolySupport.Vec d)

The homothetic copy c + (1 - lam)(U - c) of U.

Equations

• Algsuperdiff.Section3.Provider.Multiscale.shrinkToward c lam U = ⇑(AffineMap.homothety c (1 - lam)) '' U

theorem Algsuperdiff.Section3.Provider.Multiscale.volume_shrinkToward {d : ℕ} (c : HCPolySupport.Vec d) {lam : ℝ} (hlam : lam ≤ 1) (U : Set (HCPolySupport.Vec d)) : MeasureTheory.volume (shrinkToward c lam U) = ENNReal.ofReal ((1 - lam) ^ d) * MeasureTheory.volume U

theorem Algsuperdiff.Section3.Provider.Multiscale.shrinkToward_subset {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hU : Convex ℝ U) {c : HCPolySupport.Vec d} (hc : c ∈ U) {lam : ℝ} (hlam0 : 0 ≤ lam) (hlam1 : lam ≤ 1) : shrinkToward c lam U ⊆ U

theorem Algsuperdiff.Section3.Provider.Multiscale.ball_subset_of_mem_shrinkToward {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hU : Convex ℝ U) {c : HCPolySupport.Vec d} {rho lam : ℝ} (hball : Metric.ball c rho ⊆ U) (hlam0 : 0 < lam) (hlam1 : lam ≤ 1) {x : HCPolySupport.Vec d} (hx : x ∈ shrinkToward c lam U) : Metric.ball x (lam * rho) ⊆ U

The interior distance of the homothetic copy. If B(c, rho) ⊆ U and U is convex, every point of c + (1 - lam)(U - c) has its whole lam rho-ball inside U.

Total volume of a disjoint family inside a set

theorem Algsuperdiff.Section3.Provider.Multiscale.sum_cubeVolume_add_le_of_disjoint {d : ℕ} {U V : Set (HCPolySupport.Vec d)} (hUtop : MeasureTheory.volume U ≠ ⊤) (hVU : V ⊆ U) {F : Finset (HCPolySupport.TriadicCube d)} (hsub : ∀ R ∈ F, HCPolySupport.cubeSet R ⊆ U) (hdisj : (↑F).PairwiseDisjoint HCPolySupport.cubeSet) (hV : ∀ R ∈ F, Disjoint (HCPolySupport.cubeSet R) V) : ∑ R ∈ F, HCPolySupport.cubeVolume R + (MeasureTheory.volume V).toReal ≤ (MeasureTheory.volume U).toReal

Disjoint triadic cubes inside U, together with any set V ⊆ U they all avoid, use up at most the volume of U.

The depth-t volume bound for the simplex dissection

theorem Algsuperdiff.Section3.Provider.Multiscale.sum_cubeVolume_simplexDissection_le {d : ℕ} [NeZero d] (T : Whitney.KuhnCell d) (t : ℕ) {F : Finset (HCPolySupport.TriadicCube d)} (hF : ∀ R ∈ F, R ∈ simplexDissection T) (hFt : ∀ R ∈ F, R ∈ HCPolySupport.descendantsAtDepth T.supportCube t) : ∑ R ∈ F, HCPolySupport.cubeVolume R ≤ 12 * ↑d * (↑d + 1) / 3 ^ t * (MeasureTheory.volume T.openCarrier).toReal

The boundary estimate of the identified route. The cubes of the triadic Whitney dissection of an open Kuhn simplex that sit at depth t below the support cube have total volume at most 12 d (d+1) 3^{-t} times the volume of the simplex.

The proof is the convex-collar bound: at lam = 12 (d+1) 3^{-t} the homothetic copy of the simplex is farther from the complement than the diameter of a depth-(t-1) cube, while a selected cube's triadic parent meets the complement.

The weighted sum over the dissection

def Algsuperdiff.Section3.Provider.Multiscale.dissectionDepth {d : ℕ} (T : Whitney.KuhnCell d) (R : HCPolySupport.TriadicCube d) : ℕ

The depth of a dissection cube below the support cube of its simplex.

Equations

• Algsuperdiff.Section3.Provider.Multiscale.dissectionDepth T R = (T.supportCube.scale - R.scale).toNat

theorem Algsuperdiff.Section3.Provider.Multiscale.dissectionDepth_spec {d : ℕ} {T : Whitney.KuhnCell d} {R : HCPolySupport.TriadicCube d} (hR : R ∈ simplexDissection T) : R ∈ HCPolySupport.descendantsAtDepth T.supportCube (dissectionDepth T R) ∧ ↑(T.supportCube.scale - R.scale) = ↑(dissectionDepth T R)

noncomputable def Algsuperdiff.Section3.Provider.Multiscale.simplexDissectionConst (d : ℕ) (s : ℝ) : ℝ

The summability constant of the identified route, finite exactly on the window s < 1/2.

Equations

• Algsuperdiff.Section3.Provider.Multiscale.simplexDissectionConst d s = 12 * ↑d * (↑d + 1) / (1 - 3 ^ (2 * s - 1))

noncomputable def Algsuperdiff.Section3.Provider.Multiscale.simplexCrudeConst (d : ℕ) (s : ℝ) : ℝ

Half of the summability constant: the constant of the crude response bounds at the simplex carrier.

Equations

• Algsuperdiff.Section3.Provider.Multiscale.simplexCrudeConst d s = 6 * ↑d * (↑d + 1) / (1 - 3 ^ (2 * s - 1))

theorem Algsuperdiff.Section3.Provider.Multiscale.simplexDissectionConst_nonneg (d : ℕ) {s : ℝ} (hs : s < 1 / 2) : 0 ≤ simplexDissectionConst d s

theorem Algsuperdiff.Section3.Provider.Multiscale.simplexCrudeConst_nonneg (d : ℕ) {s : ℝ} (hs : s < 1 / 2) : 0 ≤ simplexCrudeConst d s

theorem Algsuperdiff.Section3.Provider.Multiscale.two_mul_simplexCrudeConst (d : ℕ) (s : ℝ) : 2 * simplexCrudeConst d s = simplexDissectionConst d s

theorem Algsuperdiff.Section3.Provider.Multiscale.tsum_cubeVolume_weight_le {d : ℕ} [NeZero d] (T : Whitney.KuhnCell d) {s : ℝ} (hs : s < 1 / 2) : ∑' (R : ↑(simplexDissection T)), ENNReal.ofReal (HCPolySupport.cubeVolume ↑R / (MeasureTheory.volume T.openCarrier).toReal * 3 ^ (2 * s * ↑(T.supportCube.scale - (↑R).scale))) ≤ ENNReal.ofReal (simplexDissectionConst d s)

The weighted sum of the identified route. For s < 1/2 the series sum_i (|R_i|/|T|) 3^{2 s t_i} over the triadic Whitney dissection of an open Kuhn simplex is bounded by the explicit d- and s-only constant 12 d (d+1) / (1 - 3^{2s-1}).

Coefficient restriction

def Algsuperdiff.Section3.Provider.Multiscale.restrictCoeffOn {d : ℕ} {U V : HCPolySupport.Book.Ch02.Domain d} (a : HCPolySupport.Book.Ch02.CoeffOn U) (h : V.carrier ⊆ U.carrier) : HCPolySupport.Book.Ch02.CoeffOn V

The restriction of a Chapter 2 coefficient object to a subdomain, with the same representative field. Literal equality of representatives is what the haS binder of l.subadd.betterer requires.

Equations

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

noncomputable def Algsuperdiff.Section3.Provider.Multiscale.simplexCoeffOn {d : ℕ} (a : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (T : Whitney.KuhnCell d) : HCPolySupport.Book.Ch02.CoeffOn (simplexDomain T)

The coefficient object on the open Kuhn simplex: the restriction of the support cube's representative.

Equations

• Algsuperdiff.Section3.Provider.Multiscale.simplexCoeffOn a T = Algsuperdiff.Section3.Provider.Multiscale.restrictCoeffOn (a.coeffOn T.supportCube) ⋯

noncomputable def Algsuperdiff.Section3.Provider.Multiscale.dissectionCoeffOn {d : ℕ} (a : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (T : Whitney.KuhnCell d) (R : ↑(simplexDissection T)) : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain ↑R)

The coefficient object on a cube of the dissection: the restriction of the same support-cube representative.

Equations

• Algsuperdiff.Section3.Provider.Multiscale.dissectionCoeffOn a T R = Algsuperdiff.Section3.Provider.Multiscale.restrictCoeffOn (a.coeffOn T.supportCube) ⋯

theorem Algsuperdiff.Section3.Provider.Multiscale.responseJ_dissectionCoeffOn {d : ℕ} (a : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (T : Whitney.KuhnCell d) (R : ↑(simplexDissection T)) (p q : HCPolySupport.Vec d) : HCPolySupport.Book.Ch02.responseJ (HCPolySupport.Book.Ch02.cubeDomain ↑R) (dissectionCoeffOn a T R) p q = HCPolySupport.Book.Ch02.responseJ (HCPolySupport.Book.Ch02.cubeDomain ↑R) (a.coeffOn ↑R) p q

On a dissection cube the restricted representative agrees a.e. with the family's own one, so the two response functionals coincide.

The crude response bounds at the simplex carrier

theorem Algsuperdiff.Section3.Provider.Multiscale.responseJ_simplexDomain_zero_flux_le_LambdaSq {d : ℕ} [NeZero d] {Q : HCPolySupport.TriadicCube d} {k : ℤ} {T : Whitney.KuhnCell d} (hT : T.supportCube ∈ HCPolySupport.descendantsAtScale Q k) (a : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) {s : ℝ} {qe : HCPolySupport.Book.Ch02.MultiscaleExponent} (hs0 : 0 < s) (hs : s < 1 / 2) (hq : qe.IsAdmissible) (p : HCPolySupport.Vec d) : HCPolySupport.Book.Ch02.responseJ (simplexDomain T) (simplexCoeffOn a T) p 0 ≤ simplexCrudeConst d s * (HCPolySupport.Book.Ch02.multiscaleDescendantWeight Q k s * HCPolySupport.Book.Ch02.LambdaSq Q s qe a) * HCPolySupport.vecNormSq p

For a Kuhn cell T whose support cube is a triadic descendant of Q at scale k, every 0 < s < 1/2 and every admissible exponent,

J(T, p, 0; a) <= C(d,s) . 3^{2 s (Q.scale - k)} . Lambda_{s,q}(Q; a) . |p|^2

with C(d,s) = simplexCrudeConst d s = 6 d (d+1) / (1 - 3^{2s-1}).

The s < 1/2 binder is the convergence window of the identified route: it is a genuine hypothesis of the boundary estimate, not a proof convenience, and the manuscript's own exponent s = 1/4 lies in it.

theorem Algsuperdiff.Section3.Provider.Multiscale.responseJ_simplexDomain_zero_slope_le_lambdaSq_inv {d : ℕ} [NeZero d] {Q : HCPolySupport.TriadicCube d} {k : ℤ} {T : Whitney.KuhnCell d} (hT : T.supportCube ∈ HCPolySupport.descendantsAtScale Q k) (a : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) {s : ℝ} {qe : HCPolySupport.Book.Ch02.MultiscaleExponent} (hs0 : 0 < s) (hs : s < 1 / 2) (hq : qe.IsAdmissible) (q : HCPolySupport.Vec d) : HCPolySupport.Book.Ch02.responseJ (simplexDomain T) (simplexCoeffOn a T) 0 q ≤ simplexCrudeConst d s * (HCPolySupport.Book.Ch02.multiscaleDescendantWeight Q k s * (HCPolySupport.Book.Ch02.lambdaSq Q s qe a)⁻¹) * HCPolySupport.vecNormSq q

The mirror of responseJ_simplexDomain_zero_flux_le_LambdaSq on the pure-flux leg.

The manuscript's exponent