HomFinitePTranslate

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

The grid-to-translate extension of a multiscale negative gauge

What this module closes

hCG' is transcribed at the PRINTED grid-summed carrier (the pure lattice 3^k ℤ^d ∩ □_m, i.e. descendantsAtDepth). The Step-3c chain consumes the gauge at EVERY TRANSLATE (UniformBoxGaugeBound), because the mollifier calculus averages against x + □_n at arbitrary centres (norm_boxMixtureVec_le_of_uniformBoxGauge). The mismatch is recorded here, and the reconstruction "grid ⟹ translate" is left unformalized.

This module proves it, at the explicit dimensional constant 6 d times the geometric factor liftGeomFactor s':

   ‖(F)_R‖ ≤ A·3^{-s' k}  for every grid cube R of scale k
     ⟹  ‖(F)_{x+□_n}‖ ≤ 6 d · liftGeomFactor s' · A · 3^{-s' n}   for EVERY x.

The mechanism is the printed one (a Whitney/greedy decomposition), and the apparatus is already in this repository: OffGridStabilityGeometry supplies

• iUnion_maximalCubes_eq — the maximal grid subcubes tile x + □_n EXACTLY;
• scale_le_of_maximalCubeIn_offGridCube — their scales are ≤ n;
• volume_iUnion_maximalCubesAtScale_toReal_le — the packing count, the total volume of the scale-k maximal cubes is at most 2d·3^{k+1-n} times the volume of the box.

Summing |Q|·A·3^{-s' k_Q} over the tiling and grouping by scale gives a geometric series in 3^{-(1-s')}, whose sum is liftGeomFactor s'; the boxes at scale k contribute 2d·3^{1+k-n}, whence 6d. Nothing else enters, and the constant is dimension-only.

liftGeomFactor s' ≤ 3 for s' ≤ 1/2 (liftGeomFactor_le_three), so the constant at the Step-3 pin is at most 18 d.

Main results

• sum_cubeVolume_fiber_le — the packing count at one scale, at 2d·3^{1-j};
• finset_sum_maximalCubes_weight_le — the packing sum, over any finite subfamily, at 6 d · liftGeomFactor s';
• abs_setIntegral_offGridCube_le — the scalar statement on an arbitrary translate of a triadic cube;
• abs_boxAverage_le_of_gridGauge, norm_boxAverageVec_le_of_gridGauge — the same at the box carrier, scalar and vector;
• uniformBoxGaugeBound_of_gridGauge — the UniformBoxGaugeBound, from the whole-grid gauge;
• gridGauge_of_descendantBound — the whole-grid gauge from the PRINTED descendants of □_m, for a field supported in □_m.

1. The packing sum

def Algsuperdiff.Section4.Provider.Homogenization.offDepth {d : ℕ} (P Q : HCPolySupport.TriadicCube d) : ℕ

The depth of a maximal cube below the shape cube of the off-grid box.

Equations

• Algsuperdiff.Section4.Provider.Homogenization.offDepth P Q = (P.scale - Q.scale).toNat

theorem Algsuperdiff.Section4.Provider.Homogenization.sum_cubeVolume_fiber_le {d : ℕ} [NeZero d] (w : HCPolySupport.Vec d) (P : HCPolySupport.TriadicCube d) (j : ℕ) (S : Finset (HCPolySupport.TriadicCube d)) (hS : ∀ Q ∈ S, ExcessDecay.MaximalCubeIn (ExcessDecay.offGridCube w P) Q ∧ Q.scale = P.scale - ↑j) : ∑ Q ∈ S, HCPolySupport.cubeVolume Q ≤ 2 * ↑d * 3 ^ (1 - ↑j) * HCPolySupport.cubeVolume P

The packing sum over one scale.

The maximal grid cubes of the off-grid box w + □_{P.scale} at depth j have total volume at most 2d·3^{1-j} times the volume of the box.

theorem Algsuperdiff.Section4.Provider.Homogenization.finset_sum_maximalCubes_weight_le {d : ℕ} [NeZero d] (w : HCPolySupport.Vec d) (P : HCPolySupport.TriadicCube d) {s' : ℝ} (hs1 : s' < 1) (S : Finset (HCPolySupport.TriadicCube d)) (hS : ∀ Q ∈ S, ExcessDecay.MaximalCubeIn (ExcessDecay.offGridCube w P) Q) : ∑ Q ∈ S, HCPolySupport.cubeVolume Q * 3 ^ (s' * (↑P.scale - ↑Q.scale)) ≤ 6 * ↑d * liftGeomFactor s' * HCPolySupport.cubeVolume P

THE PACKING SUM.

Over any finite subfamily of the maximal grid cubes of the off-grid box w + □_{P.scale}, the volume-weighted sum of 3^{s'·depth} is at most 6 d · liftGeomFactor s' times the volume of the box. This is the whole geometric content of the grid-to-translate extension.

2. The tiling turns the packing sum into an average bound

theorem Algsuperdiff.Section4.Provider.Homogenization.abs_setIntegral_offGridCube_le {d : ℕ} [NeZero d] (w : HCPolySupport.Vec d) (P : HCPolySupport.TriadicCube d) {s' A : ℝ} (hs1 : s' < 1) (hA : 0 ≤ A) {f : HCPolySupport.Vec d → ℝ} (hf : MeasureTheory.Integrable f MeasureTheory.volume) (hgrid : ∀ (Q : HCPolySupport.TriadicCube d), Q.scale ≤ P.scale → |HCPolySupport.cubeAverage Q f| ≤ A * 3 ^ (-(s' * ↑Q.scale))) : |∫ (y : HCPolySupport.Vec d) in ExcessDecay.offGridCube w P, f y| ≤ 6 * ↑d * liftGeomFactor s' * A * 3 ^ (-(s' * ↑P.scale)) * HCPolySupport.cubeVolume P

The grid-to-translate estimate, scalar form.

If every grid cube average of f obeys the multiscale bound A·3^{-s' k}, then so does the average over an ARBITRARY real translate of a triadic cube, at the dimensional cost 6 d · liftGeomFactor s'.

3. The box carrier

theorem Algsuperdiff.Section4.Provider.Homogenization.offGridCube_originCube_eq_ball {d : ℕ} (n : ℤ) (x : HCPolySupport.Vec d) : ExcessDecay.offGridCube x (HCPolySupport.originCube d n) = Metric.ball x (boxRadius n)

The scale-n box centred at x is the off-grid cube of shape □_n.

theorem Algsuperdiff.Section4.Provider.Homogenization.abs_boxAverage_le_of_gridGauge {d : ℕ} [NeZero d] {n : ℤ} {s' A : ℝ} (hs1 : s' < 1) (hA : 0 ≤ A) {f : HCPolySupport.Vec d → ℝ} (hf : MeasureTheory.Integrable f MeasureTheory.volume) (hgrid : ∀ (Q : HCPolySupport.TriadicCube d), Q.scale ≤ n → |HCPolySupport.cubeAverage Q f| ≤ A * 3 ^ (-(s' * ↑Q.scale))) (x : HCPolySupport.Vec d) : |boxAverage n x f| ≤ 6 * ↑d * liftGeomFactor s' * A * 3 ^ (-(s' * ↑n))

The grid-to-translate estimate at the box carrier, scalar form.

theorem Algsuperdiff.Section4.Provider.Homogenization.norm_boxAverageVec_le_of_gridGauge {d : ℕ} [NeZero d] {n : ℤ} {s' A : ℝ} (hs1 : s' < 1) (hA : 0 ≤ A) {F : HCPolySupport.Vec d → HCPolySupport.Vec d} (hF : ∀ (i : Fin d), MeasureTheory.Integrable (fun (y : HCPolySupport.Vec d) => F y i) MeasureTheory.volume) (hgrid : ∀ (Q : HCPolySupport.TriadicCube d), Q.scale ≤ n → ‖HCPolySupport.cubeAverageVec Q F‖ ≤ A * 3 ^ (-(s' * ↑Q.scale))) (x : HCPolySupport.Vec d) : ‖boxAverageVec n x F‖ ≤ 6 * ↑d * liftGeomFactor s' * A * 3 ^ (-(s' * ↑n))

The grid-to-translate estimate at the box carrier, vector form.

theorem Algsuperdiff.Section4.Provider.Homogenization.uniformBoxGaugeBound_of_gridGauge {d : ℕ} [NeZero d] (m : ℤ) {s' A : ℝ} (hs1 : s' < 1) (hA : 0 ≤ A) {F : HCPolySupport.Vec d → HCPolySupport.Vec d} (hF : ∀ (i : Fin d), MeasureTheory.Integrable (fun (y : HCPolySupport.Vec d) => F y i) MeasureTheory.volume) (hgrid : ∀ (Q : HCPolySupport.TriadicCube d), Q.scale ≤ m → ‖HCPolySupport.cubeAverageVec Q F‖ ≤ A * 3 ^ (-(s' * ↑Q.scale))) : UniformBoxGaugeBound m s' (6 * ↑d * liftGeomFactor s' * A) F

THE GRID-TO-TRANSLATE EXTENSION.

A multiscale negative gauge of order -s' on the PRINTED triadic grid — every grid cube of every scale — is the translate-uniform UniformBoxGaugeBound at the dimensional cost 6 d · liftGeomFactor s'. For s' ≤ 1/2 the geometric factor is at most 3, so the cost is at most 18 d.

This is the item left open above; the source hypothesis may therefore be transcribed at the printed grid carrier and consumed at the translate carrier without any harvest.

4. From the PRINTED descendants to the whole grid

theorem Algsuperdiff.Section4.Provider.Homogenization.gridGauge_of_descendantBound {d : ℕ} (m : ℤ) {s' A : ℝ} (hA : 0 ≤ A) {F : HCPolySupport.Vec d → HCPolySupport.Vec d} (hzero : ∀ y ∉ HCPolySupport.cubeSet (HCPolySupport.originCube d m), F y = 0) (hdesc : ∀ (j : ℕ), ∀ R ∈ HCPolySupport.descendantsAtDepth (HCPolySupport.originCube d m) j, ‖HCPolySupport.cubeAverageVec R F‖ ≤ A * 3 ^ (-(s' * ↑R.scale))) (Q : HCPolySupport.TriadicCube d) : Q.scale ≤ m → ‖HCPolySupport.cubeAverageVec Q F‖ ≤ A * 3 ^ (-(s' * ↑Q.scale))

The printed carrier feeds the whole-grid hypothesis.

The printed sum of the negative Besov seminorm definition runs over 3^k ℤ^d ∩ □_m, i.e. over the triadic descendants of □_m; uniformBoxGaugeBound_of_gridGauge asks for every grid cube of scale ≤ m. The two agree for a field supported in □_m: a grid cube of scale ≤ m either shares a point with □_m, and is then a descendant of it (nested-or-disjoint), or is disjoint from it, and then its average vanishes.

The support hypothesis is the H¹₀ zero extension already present in the frame — the Step-3 object is ∇(u-v) with u - v ∈ H¹₀(□_m).