CubeSchauderAeCutoff

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

Cube Schauder: the cutoff pairing of the a.e. identification

CubeSchauderAssembly.exists_zeroDatumWitness_of_campanato consumes the almost-everywhere identification Ψ = ∇w of the Campanato slope field with the H¹ weak gradient. The quantitative half of that identification is the statement proved here: for the smooth cutoff η that is 1 on the Euclidean ball of radius 3^j/8 around z and supported in the ball of radius 3^j/4,

  |∫_{□_m} (∂_i w − g_i) η|  =  |∫_{□_m} (w − ℓ) ∂_i η|
                             ≤  C(d)·3^{-j}·‖w − ℓ‖_{L²(W_j)}·|W_j| ,

where ℓ = (c,g) is any affine competitor and W_j = (z+□_j) ∩ □_m. Fed with the affine minimizer of the window and the Campanato datum E(w, W_j) ≤ K√(3^j), the right-hand side is C(d)·K·√(3^j)·|W_j|, which is o(|W_j|) — the ingredient the Lebesgue-point argument needs.

The three components are:

• setIntegral_abs_le_sqrt_mul_sqrt — the L¹ ≤ L² comparison on a window of finite positive measure, proved from the elementary two-parameter bound |f| ≤ (t f² + t⁻¹)/2 optimized at t = √|W| / ‖f‖_{L²}. (The repository had no volume-average Cauchy–Schwarz; see Support.NormalizedL2's note.)
• campanatoCutoff — CoarseGraining's quantitative ball cutoff at the radii 3^j/8 and 3^j/4, together with the six facts the pairing needs.
• integral_grad_sub_slope_mul_cutoff — the integration-by-parts identity, the weak-gradient identity of w minus the same identity for the smooth affine competitor, and abs_integral_grad_sub_slope_mul_cutoff_le — its bound.

References

• ABK26.

1. The L¹ ≤ L² comparison on a window

theorem Algsuperdiff.Section4.Provider.Schauder.setIntegral_abs_le_sqrt_mul_sqrt {d : ℕ} {W : Set (HCPolySupport.Vec d)} (hWfin : MeasureTheory.volume W ≠ ⊤) (hWpos : 0 < (MeasureTheory.volume W).toReal) {f : HCPolySupport.Vec d → ℝ} (hf : MeasureTheory.MemLp f 2 (MeasureTheory.volume.restrict W)) : ∫ (y : HCPolySupport.Vec d) in W, |f y| ≤ √(∫ (y : HCPolySupport.Vec d) in W, f y ^ 2) * √(MeasureTheory.volume W).toReal

L¹ ≤ L² on a window of finite positive measure.

∫_W |f| ≤ ‖f‖_{L²(W)}·|W|^{1/2}. Proved from the elementary pointwise bound |f| ≤ (t f² + t⁻¹)/2, integrated and optimized at t = |W|^{1/2}/‖f‖_{L²(W)}; the degenerate branch ‖f‖_{L²(W)} = 0 is handled separately.

theorem Algsuperdiff.Section4.Provider.Schauder.sqrt_setIntegral_sq_eq_normalizedL2On {d : ℕ} {W : Set (HCPolySupport.Vec d)} (hWpos : 0 < (MeasureTheory.volume W).toReal) (f : HCPolySupport.Vec d → ℝ) : √(∫ (y : HCPolySupport.Vec d) in W, f y ^ 2) = Support.normalizedL2On W f * √(MeasureTheory.volume W).toReal

√(∫_W f²) = ‖f‖_{L²(W)}·√|W| on a window of finite positive measure.

2. The Campanato cutoff

noncomputable def Algsuperdiff.Section4.Provider.Schauder.campanatoCutoff {d : ℕ} (z : HCPolySupport.Vec d) (j : ℤ) : HCPolySupport.Vec d → ℝ

The Campanato cutoff at z and scale j: CoarseGraining's quantitative ball cutoff, equal to 1 on the Euclidean ball of radius 3^j/8 and supported in the ball of radius 3^j/4.

Equations

• Algsuperdiff.Section4.Provider.Schauder.campanatoCutoff z j = HCPolySupport.QuantitativeBallCutoff.canonicalFun z (3 ^ j / 8) (3 ^ j / 4)

theorem Algsuperdiff.Section4.Provider.Schauder.campanatoCutoff_smooth {d : ℕ} (z : HCPolySupport.Vec d) (j : ℤ) : ContDiff ℝ (↑⊤) (campanatoCutoff z j)

theorem Algsuperdiff.Section4.Provider.Schauder.campanatoCutoff_hasCompactSupport {d : ℕ} (z : HCPolySupport.Vec d) (j : ℤ) : HasCompactSupport (campanatoCutoff z j)

theorem Algsuperdiff.Section4.Provider.Schauder.campanatoCutoff_nonneg {d : ℕ} (z : HCPolySupport.Vec d) (j : ℤ) (y : HCPolySupport.Vec d) : 0 ≤ campanatoCutoff z j y

theorem Algsuperdiff.Section4.Provider.Schauder.campanatoCutoff_le_one {d : ℕ} (z : HCPolySupport.Vec d) (j : ℤ) (y : HCPolySupport.Vec d) : campanatoCutoff z j y ≤ 1

theorem Algsuperdiff.Section4.Provider.Schauder.campanatoCutoff_eq_one {d : ℕ} {z : HCPolySupport.Vec d} {j : ℤ} {y : HCPolySupport.Vec d} (hy : y ∈ HCPolySupport.euclideanBall z (3 ^ j / 8)) : campanatoCutoff z j y = 1

theorem Algsuperdiff.Section4.Provider.Schauder.campanatoCutoff_tsupport_subset {d : ℕ} (z : HCPolySupport.Vec d) (j : ℤ) : tsupport (campanatoCutoff z j) ⊆ HCPolySupport.euclideanBall z (3 ^ j / 2)

noncomputable def Algsuperdiff.Section4.Provider.Schauder.cutoffIbpConst (d : ℕ) : ℝ

The constant of the cutoff pairing: 16·d·θ', where θ' is the transition profile's derivative bound.

Equations

• Algsuperdiff.Section4.Provider.Schauder.cutoffIbpConst d = 16 * ↑d * HCPolySupport.smoothTransitionProfile.derivBound

theorem Algsuperdiff.Section4.Provider.Schauder.cutoffIbpConst_nonneg (d : ℕ) : 0 ≤ cutoffIbpConst d

theorem Algsuperdiff.Section4.Provider.Schauder.norm_fderiv_campanatoCutoff_le {d : ℕ} (z : HCPolySupport.Vec d) (j : ℤ) (y : HCPolySupport.Vec d) : ‖fderiv ℝ (campanatoCutoff z j) y‖ ≤ cutoffIbpConst d * 3 ^ (-j)

theorem Algsuperdiff.Section4.Provider.Schauder.abs_fderiv_campanatoCutoff_apply_le {d : ℕ} (z : HCPolySupport.Vec d) (j : ℤ) (y : HCPolySupport.Vec d) (i : Fin d) : |(fderiv ℝ (campanatoCutoff z j) y) (HCPolySupport.basisVec i)| ≤ cutoffIbpConst d * 3 ^ (-j)

theorem Algsuperdiff.Section4.Provider.Schauder.fderiv_campanatoCutoff_eq_zero {d : ℕ} {z : HCPolySupport.Vec d} {j : ℤ} {y : HCPolySupport.Vec d} (hy : y ∉ HCPolySupport.euclideanBall z (3 ^ j / 2)) : fderiv ℝ (campanatoCutoff z j) y = 0

Off the Euclidean ball of radius 3^j/2 the cutoff's derivative vanishes.

theorem Algsuperdiff.Section4.Provider.Schauder.euclideanBall_subset_image_add_openCubeSet {d : ℕ} (z : HCPolySupport.Vec d) (j : ℤ) : HCPolySupport.euclideanBall z (3 ^ j / 2) ⊆ (fun (y : HCPolySupport.Vec d) => z + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d j)

The Euclidean ball is contained in the sup-metric cube of the same radius, hence in the translated triadic cube of scale j.