OscillationPoincare

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

The function-level multiscale Poincare estimate on a triadic cube

This module bounds the normalized L^2 oscillation of a W^{1,2} function on a triadic cube directly by the multiscale sum of the cube averages of its gradient, without passing through any negative Sobolev or negative Besov norm of the gradient.

The manuscript reaches the same right-hand side in two moves: the duality step, ‖v-(v)_{\cu_m}‖_{\underline L^2(\cu_m)} ≤ C‖∇v‖_{\Hminusul(\cu_m)}, followed by the multiscale Poincare inequality of AK.Book, Proposition 1.10. The first move is a Necas-type inequality that is not available upstream at the zero-boundary primitive. The composition of the two moves, however, is available upstream in one piece, and that composition is what this module assembles.

Route

1. Homogenization.CubeDualFullVectorPoincareEstimate.of_h1Function (Homogenization/Sobolev/Foundations/CubeBesovPoincare.lean) bounds cubeBesovOscillation Q 2 u by fullVectorPoincareCubeConstant Q times the coordinate sum of the full negative Besov dual norms cubeBesovDualFullNorm Q 1 2 1 (∂_i u). This is the upstream oscillation-by-dual-gradient estimate: its own proof solves the cube Neumann Poisson problem and pays the Neumann Calderon-Zygmund constant, so it is the analytic content of the manuscript's duality step, at the negative Besov dual rather than at \Hminusul. Its constant is dimension-only and independent of the cube (fullVectorPoincareCubeConstant_eq_dimensionConstant).
2. Homogenization.cubeBesovDualFullNorm_le_note_constant_mul_cubeBesovCircNorm (Homogenization/Besov/Duality/GlobalComparison.lean) at (s,p,q) = (1,2,1) bounds each such dual norm by 3^{d+1} times the negative circ norm cubeBesovCircNorm Q 1 2 1 (∂_i u). This is the same upstream comparison, at the same exponents, that the proved multiscale Poincare bridge of MultiscalePoincareBridge.lean uses on its own right-hand side.
3. Multiplying by the cube scale weight 3^{-m} puts the estimate in the manuscript's scaled display.
4. The normalized L^2 square carried by the coarse-grained Caccioppoli right-hand side, Ch03.interiorCaccioppoliParentOscillationL2Sq, is the square of that oscillation, so the last two theorems deliver the Caccioppoli right-hand side in multiscale form for an arbitrary Chapter 2 cube solution.

Upstream sibling

Homogenization.Book.Ch01.Legacy.h1_descendantLocalFullCircPoincare (Homogenization/Book/Ch01/Theorems/MultiscalePoincare.lean) composes the same two upstream steps, with the same constant, on every descendant of a cube at once, for the parent fluctuation of the function. This module therefore takes the two upstream endpoints directly, at the single cube and for the function itself, rather than specializing that lane.

Correspondence with the printed display

MultiscalePoincareBridge.cubeBesovCircDepthWeight_one records that at s = 1 the depth-j negative circ weight of a cube of scale m is 3^{m-j}, so 3^{-m}·cubeBesovCircNorm Q 1 2 1 f is the printed sum Σ_{n ≤ m} 3^{-(m-n)}(avsum_z |(f)_{z+\cu_n}|^2)^{1/2} under the reindexing n = m - j. That identification is a formalization reading of the upstream definitions, inherited unchanged from the proved bridge and not re-derived here.

The coordinate aggregation here is the plain sum over coordinates of the per-coordinate multiscale sums. The printed display aggregates the coordinates inside each depth term, in the Euclidean norm of the vector average. Cauchy's inequality in the coordinate index converts the aggregation used here into the printed one at the cost of a factor \sqrt d, which a dimension-only constant absorbs; that conversion is not formalized here.

What is and is not estimated here

The estimate proved here has the multiscale average sum on its right-hand side, not the manuscript's 3^{-2m}‖∇v‖_{\Hminusul(\cu_m)}^2. The two are not interchangeable: the proved bridge MultiscalePoincareBridge.scaledNegHMinusOne_le_multiscaleAverageSum bounds the negative Sobolev object by the multiscale sum, so the right-hand side here is the upstream bound of the printed one and is therefore weaker. No reverse comparison is claimed, and no negative Sobolev or negative Besov norm occurs in any statement of this module. The bridge's own right-hand side is the Euclidean coordinate aggregate of the same circ norms, which lies below the coordinate sum used here; the comparison is therefore in the stated direction only up to the √d coordinate aggregation, and no declaration in this directory compares the negative Sobolev object to the multiscale average sum directly.

The centred variant, in which each coordinate circ norm is taken of ∂_i v - c_i for a comparison vector c, is not proved here. It follows from the estimate proved here together with the depthwise triangle inequality (avsum_z |(f)_{z+\cu_n}|^2)^{1/2} ≤ (avsum_z |(f-c)_{z+\cu_n}|^2)^{1/2} + |c| summed against the circ weights, whose total is at most (3/2)·3^m; that step is left to the consumer, where the |c| term meets the term the manuscript already carries.

The dimensional constant

noncomputable def Algsuperdiff.Section3.Provider.Besov.oscillationMultiscalePoincareConstant (d : ℕ) : ℝ

The scale-free dimensional constant of the function-level multiscale Poincare estimate: the cube full-dual vector Poincare constant times the upstream full-dual-to-circ comparison constant at s = 1.

Equations

• Algsuperdiff.Section3.Provider.Besov.oscillationMultiscalePoincareConstant d = ↑d * HCPolySupport.Legacy.cubeNeumannW22CalderonZygmundConstant d * 3 ^ (↑d + 1)

theorem Algsuperdiff.Section3.Provider.Besov.oscillationMultiscalePoincareConstant_nonneg (d : ℕ) : 0 ≤ oscillationMultiscalePoincareConstant d

The oscillation bound

theorem Algsuperdiff.Section3.Provider.Besov.cubeBesovOscillation_le_oscillationMultiscalePoincareConstant_mul_sum_cubeBesovCircNorm {d : ℕ} (Q : HCPolySupport.TriadicCube d) (u : HCPolySupport.H1Function (HCPolySupport.openCubeSet Q)) : (HCPolySupport.cubeBesovOscillation Q 2 fun (x : HCPolySupport.Vec d) => u.toFun x) ≤ oscillationMultiscalePoincareConstant d * ∑ i : Fin d, HCPolySupport.cubeBesovCircNorm Q 1 2 1 fun (x : HCPolySupport.Vec d) => u.grad x i

The function-level multiscale Poincare estimate. The normalized L² oscillation of a W^{1,2} function on a triadic cube is bounded by a scale-free dimensional constant times the sum over coordinates of the negative circ Besov norm at (s,p,q) = (1,2,1) of the corresponding partial derivative, which is the manuscript's multiscale sum of gradient cube averages for that coordinate, weighted by 3^{Q.scale}.

The Caccioppoli right-hand side

theorem Algsuperdiff.Section3.Provider.Besov.normalizedL2SqOnSet_openCubeSet_centred_eq_cubeBesovOscillation_sq {d : ℕ} (Q : HCPolySupport.TriadicCube d) (u : HCPolySupport.H1Function (HCPolySupport.openCubeSet Q)) : (HCPolySupport.Book.Ch03.normalizedL2SqOnSet (HCPolySupport.openCubeSet Q) fun (x : HCPolySupport.Vec d) => u.toFun x - HCPolySupport.cubeAverage Q fun (x : HCPolySupport.Vec d) => u.toFun x) = (HCPolySupport.cubeBesovOscillation Q 2 fun (x : HCPolySupport.Vec d) => u.toFun x) ^ 2

The normalized L² square of the centred function on the open cube, which is the carrier of the Caccioppoli right-hand side, is the square of the cube oscillation.

theorem Algsuperdiff.Section3.Provider.Besov.interiorCaccioppoliParentOscillationL2Sq_le_sq_sum_cubeBesovCircNorm {d : ℕ} (Q : HCPolySupport.TriadicCube d) (a : HCPolySupport.Book.Ch03.CoeffFamily d) (v : HCPolySupport.Book.Ch03.CubeSolution Q a) : HCPolySupport.Book.Ch03.interiorCaccioppoliParentOscillationL2Sq Q a v ≤ (oscillationMultiscalePoincareConstant d * ∑ i : Fin d, HCPolySupport.cubeBesovCircNorm Q 1 2 1 fun (x : HCPolySupport.Vec d) => v.toH1.grad x i) ^ 2

The Caccioppoli right-hand side in multiscale form. The parent-cube oscillation L² square that the coarse-grained Caccioppoli estimate leaves on the right is bounded by the square of the coordinate-summed multiscale average sum of the solution gradient.