TruncationPoincareBridge

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

The per-truncation form of the coarse-grained Poincare inequality

ABK26 Proposition p.coarse.grained.Poincare is available in CoarseGraining as coarsePoincareGradient_negativeBesov_le and coarsePoincareFlux_negativeBesov_le, but stated with the public Chapter-3 seminorm scaleNormalizedNegativeBesovVectorNorm, whose q = 2 instance is a supremum over truncations N. The doubled-variables reformulation e.CG.Poincare.doubled.vars needs the inequality in a form that can be combined with the triangle inequality, and CoarseGraining's q = 2 triangle inequality is a per-truncation statement whose supremum form additionally requires the truncated seminorms to be bounded above. This module supplies that -- item (gamma) of the infrastructure list recorded in DoubledEnergyIdentity.lean:

• the identification of the public q = 2 seminorm with CoarseGraining's concrete truncated q = 2 seminorm, truncation by truncation;
• the boundedness of the truncated seminorms of a solution gradient and of a solution flux, from their L^2 membership;
• the two coarse Poincare bounds restated on the concrete seminorm.

The exponent window

The q = 2 bounds below are stated for s in (0,1). Recorded here so the deviation is visible at the point of use.

Main results

• negativeBesovVectorPartialNormFinite_two_eq, scaleNormalizedNegativeBesovVectorNorm_finite_two_eq -- the identification.
• cubeBesovNegativeVectorPartialSeminormTwo_bddAbove_of_memVectorL2 -- the truncation bound.
• solutionGradientField_memVectorL2, solutionFluxField_memVectorL2 and the two bddAbove corollaries.
• cubeBesovNegativeVectorSeminormTwo_solutionGradientField_le and cubeBesovNegativeVectorSeminormTwo_solutionFluxField_le -- the two halves of p.coarse.grained.Poincare on the concrete seminorm.

Scope

No anchor, frozen theorem or external input is consumed, and there is no sorry.

References

• ABK26, p.coarse.grained.Poincare; r.cg.poincare.doubled.variables.

Identification of the public q = 2 seminorm

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.negativeBesovVectorPartialNormFinite_two_eq {d : ℕ} (Q : HCPolySupport.TriadicCube d) (s : ℝ) (N : ℕ) (F : HCPolySupport.Vec d → HCPolySupport.Vec d) : HCPolySupport.Book.Ch03.negativeBesovVectorPartialNormFinite Q s 2 N F = HCPolySupport.cubeBesovNegativeVectorPartialSeminormTwo Q s N F

Per-truncation identification. At q = 2 the public truncated Besov norm is CoarseGraining's concrete truncated q = 2 seminorm.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.scaleNormalizedNegativeBesovVectorNorm_finite_two_eq {d : ℕ} (Q : HCPolySupport.TriadicCube d) (s : ℝ) (F : HCPolySupport.Vec d → HCPolySupport.Vec d) : HCPolySupport.Book.Ch03.scaleNormalizedNegativeBesovVectorNorm Q s (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) F = HCPolySupport.cubeBesovNegativeVectorSeminormTwo Q s F

The supremum form of the identification.

The truncation bound

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.cubeBesovNegativeVectorPartialSeminormTwo_bddAbove_of_memVectorL2 {d : ℕ} (Q : HCPolySupport.TriadicCube d) {s : ℝ} (hs : 0 < s) (u : HCPolySupport.Vec d → HCPolySupport.Vec d) (hu : HCPolySupport.MemVectorL2 (HCPolySupport.cubeSet Q) u) : BddAbove (Set.range fun (N : ℕ) => HCPolySupport.cubeBesovNegativeVectorPartialSeminormTwo Q s N u)

The truncated seminorms of an L^2 field are bounded above. This is what makes the supremum form of the q = 2 triangle inequality available.

L^2 membership of the two solution fields

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.solutionGradientField_memVectorL2 {d : ℕ} (Q : HCPolySupport.TriadicCube d) (a : HCPolySupport.Book.Ch03.CoeffFamily d) (u : HCPolySupport.Book.Ch03.CubeSolution Q a) : HCPolySupport.MemVectorL2 (HCPolySupport.cubeSet Q) (HCPolySupport.Book.Ch03.solutionGradientField u)

The gradient of a cube solution is in L^2 of the closed cube.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.solutionFluxField_memVectorL2 {d : ℕ} (Q : HCPolySupport.TriadicCube d) (a : HCPolySupport.Book.Ch03.CoeffFamily d) (u : HCPolySupport.Book.Ch03.CubeSolution Q a) : HCPolySupport.MemVectorL2 (HCPolySupport.cubeSet Q) (HCPolySupport.Book.Ch03.solutionFluxField Q a u)

The flux of a cube solution is in L^2 of the closed cube: the pointwise representative of the coefficient field is uniformly elliptic on the cube, and the flux agrees with the representative's flux almost everywhere.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.solutionGradientField_bddAbove {d : ℕ} (Q : HCPolySupport.TriadicCube d) (a : HCPolySupport.Book.Ch03.CoeffFamily d) {s : ℝ} (hs : 0 < s) (u : HCPolySupport.Book.Ch03.CubeSolution Q a) : BddAbove (Set.range fun (N : ℕ) => HCPolySupport.cubeBesovNegativeVectorPartialSeminormTwo Q s N (HCPolySupport.Book.Ch03.solutionGradientField u))

Truncation bound for the gradient field.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.solutionFluxField_bddAbove {d : ℕ} (Q : HCPolySupport.TriadicCube d) (a : HCPolySupport.Book.Ch03.CoeffFamily d) {s : ℝ} (hs : 0 < s) (u : HCPolySupport.Book.Ch03.CubeSolution Q a) : BddAbove (Set.range fun (N : ℕ) => HCPolySupport.cubeBesovNegativeVectorPartialSeminormTwo Q s N (HCPolySupport.Book.Ch03.solutionFluxField Q a u))

Truncation bound for the flux field.

p.coarse.grained.Poincare on the concrete seminorm

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.cubeBesovNegativeVectorSeminormTwo_solutionGradientField_le {d : ℕ} [NeZero d] (Q : HCPolySupport.TriadicCube d) (a : HCPolySupport.Book.Ch03.CoeffFamily d) {s : ℝ} (u : HCPolySupport.Book.Ch03.CubeSolution Q a) (hs : 0 < s) (_hs1 : s < 1) : HCPolySupport.cubeBesovNegativeVectorSeminormTwo Q s (HCPolySupport.Book.Ch03.solutionGradientField u) ≤ HCPolySupport.Book.Ch03.poincareDiscountFactor s (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) * HCPolySupport.Book.Ch03.poincareLowerEllipticityFactor Q a s (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) * HCPolySupport.Book.Ch03.solutionEnergyNorm Q a u

e.besov.grad.poincare at q = 2, on the concrete seminorm. For s in (0,1),

[grad u]_{B^{-s}_{2,2}(Q)} <= c_{s,2}^{-1/2} lambda_{s,2}^{-1/2}(Q;a) || sigma^{1/2} grad u ||_{L^2(Q)}.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.cubeBesovNegativeVectorSeminormTwo_solutionFluxField_le {d : ℕ} [NeZero d] (Q : HCPolySupport.TriadicCube d) (a : HCPolySupport.Book.Ch03.CoeffFamily d) {s : ℝ} (u : HCPolySupport.Book.Ch03.CubeSolution Q a) (hs : 0 < s) (_hs1 : s < 1) : HCPolySupport.cubeBesovNegativeVectorSeminormTwo Q s (HCPolySupport.Book.Ch03.solutionFluxField Q a u) ≤ HCPolySupport.Book.Ch03.poincareDiscountFactor s (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) * HCPolySupport.Book.Ch03.poincareUpperEllipticityFactor Q a s (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) * HCPolySupport.Book.Ch03.solutionEnergyNorm Q a u

e.besov.flux.poincare at q = 2, on the concrete seminorm. For s in (0,1),

[a grad u]_{B^{-s}_{2,2}(Q)} <= c_{s,2}^{-1/2} Lambda_{s,2}^{1/2}(Q;a) || sigma^{1/2} grad u ||_{L^2(Q)}.