ConstantDatumCorrector

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

The zero-trace corrector of a cube, at the ellipticity constants it really has

This module prepares the constant-datum comparison route of the anchor's general clause in the interior (frontier-empty) regime.

  -∇ · a∇ρ = -∇ · g   in Q ,      ρ ∈ H¹₀(Q) ,

and the module records the two bounds the route needs, with the coarse-grained ellipticity constants left in place:

• exists_correctorParentEnergy_le — the parent-cube coefficient energy of ρ, from CoarseGraining's zero-Dirichlet energy estimate: ⨍_Q ∇ρ·a∇ρ ≤ K t^{-3} λ_{t,2}^{-1} [g]²_{B^{2t}(Q)};
• exists_correctorParentL2_forceScale — the parent-cube L² value of ρ, through the negative-norm chain (NegNormToL2.cubeLpNorm_h10_le_negativeBesov_quarter composed with CoarseGraining's coarse Poincaré with right-hand side): 3^{-2 m} ‖ρ‖²_{L²(Q)} ≤ K (t^{-3} λ_{t,2}^{-1} [g]_{B^{2t}(Q)})².

Why not CoarseGraining's own parent-L² bridge (disclosed)

CoarseGraining performs exactly this composition inside the proof of its coarse Caccioppoli with right-hand side, but its internal bridge is stated at t^{-8} λ_{t,1}^{-1} [g]² — it spends λ_{t,1} λ_{t,2}^{-2} ≤ A t^{-2} λ_{t,1}^{-1}, a deterministic comparison of the two lower-ellipticity constants which costs a factor t^{-2}. The two theorems below therefore re-run CoarseGraining's composition from its public parts and stop before the ellipticity comparison, leaving λ_{t,2}^{-1} visible for the caller to discharge from the good event.

Nothing here is a new analytic input: every step is a public CoarseGraining theorem or the proved NegNormToL2/L2Bridge bridge.

References

• ABK26, l.coarse.grained.Caccioppoli.RHS; e.energy.bound.interior.

2. The corrector exists at the cube's own coefficient family

noncomputable def Algsuperdiff.Section4.Provider.ExcessDecay.constantDatumCorrector {d : ℕ} [NeZero d] (Q : HCPolySupport.TriadicCube d) (a : HCPolySupport.Book.Ch03.CoeffFamily d) {g : HCPolySupport.Vec d → HCPolySupport.Vec d} (hg : HCPolySupport.MemVectorL2 (HCPolySupport.cubeSet Q) g) : HCPolySupport.ZeroTraceDirichletCorrectorData Q (HCPolySupport.Book.Ch03.publicCoeffField Q a) g

The zero-trace corrector of the cube. CoarseGraining's canonical Dirichlet corrector at the everywhere-elliptic representative of the family.

Equations

• Algsuperdiff.Section4.Provider.ExcessDecay.constantDatumCorrector Q a hg = HCPolySupport.zeroTraceDirichletCorrectorDataOfCubeEllipticity Q hg ⋯

3. The parent-cube energy of the corrector

theorem Algsuperdiff.Section4.Provider.ExcessDecay.exists_correctorParentEnergy_le (d : ℕ) [NeZero d] : ∃ (K : ℝ), 0 < K ∧ ∀ {Q : HCPolySupport.TriadicCube d} {a : HCPolySupport.Book.Ch03.CoeffFamily d} {t : ℝ} {g : HCPolySupport.Vec d → HCPolySupport.Vec d} (rho : HCPolySupport.ZeroTraceDirichletCorrectorData Q (HCPolySupport.Book.Ch03.publicCoeffField Q a) g), 0 < t → t < 1 / 2 → HCPolySupport.Book.Ch03.ForceBesovRegularity Q (2 * t) g → HCPolySupport.Book.Ch03.localizedCoeffEnergyValue (HCPolySupport.openCubeSet Q) (a.coeffOn Q) (HCPolySupport.Book.Ch03.boundaryForcedCaccioppoliCorrectorOpenH10 rho).toH1Function ≤ K * (t.rpow (-3) * (HCPolySupport.Book.Ch02.lambdaSq Q t (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a).rpow (-1) * HCPolySupport.Book.Ch03.scaleNormalizedPositiveBesovVectorSeminormTwo Q (2 * t) g ^ 2)

The corrector's parent energy, at CoarseGraining's zero-Dirichlet force scale.

⨍_Q ∇ρ · a ∇ρ ≤ K t^{-3} λ_{t,2}^{-1} [g]²_{B^{2t}(Q)}. This is CoarseGraining's zeroDirichletEnergyWithRHSRHS, squared; no ellipticity comparison is made.

4. The corrector's negative-norm bound, at the same force scale

theorem Algsuperdiff.Section4.Provider.ExcessDecay.exists_correctorNegativeBesov_le (d : ℕ) [NeZero d] : ∃ (K : ℝ), 0 < K ∧ ∀ {Q : HCPolySupport.TriadicCube d} {a : HCPolySupport.Book.Ch03.CoeffFamily d} {t : ℝ} {g : HCPolySupport.Vec d → HCPolySupport.Vec d} (rho : HCPolySupport.ZeroTraceDirichletCorrectorData Q (HCPolySupport.Book.Ch03.publicCoeffField Q a) g), 0 < t → t < 1 / 2 → HCPolySupport.Book.Ch03.ForceBesovRegularity Q (2 * t) g → (HCPolySupport.cubeBesovNegativeVectorSeminormTwo Q (2 * t) fun (x : HCPolySupport.Vec d) => rho.toH10.grad x) ≤ K * (t.rpow (-3) * (HCPolySupport.Book.Ch02.lambdaSq Q t (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a).rpow (-1) * HCPolySupport.Book.Ch03.scaleNormalizedPositiveBesovVectorSeminormTwo Q (2 * t) g)

The corrector's gradient in the negative Besov norm.

CoarseGraining's coarse Poincaré with right-hand side, applied to the corrector and closed with its own zero-Dirichlet energy estimate: [∇ρ]_{B^{-2t}(Q)} ≤ K t^{-3} λ_{t,2}^{-1} [g]_{B^{2t}(Q)}. This is CoarseGraining's own coarsePoincareWithRHSGradientRHS_le_corrector_forceScale, read at the concrete seminorm carrier.

5. The corrector's parent L² value, at the same force scale

theorem Algsuperdiff.Section4.Provider.ExcessDecay.exists_correctorParentL2_forceScale (d : ℕ) [NeZero d] : ∃ (K : ℝ), 0 < K ∧ ∀ {Q : HCPolySupport.TriadicCube d} {a : HCPolySupport.Book.Ch03.CoeffFamily d} {t : ℝ} {g : HCPolySupport.Vec d → HCPolySupport.Vec d} (rho : HCPolySupport.ZeroTraceDirichletCorrectorData Q (HCPolySupport.Book.Ch03.publicCoeffField Q a) g), 0 < t → t ≤ 1 / 4 → HCPolySupport.Book.Ch03.ForceBesovRegularity Q (2 * t) g → Real.rpow 3 (-2 * ↑Q.scale) * HCPolySupport.Book.Ch03.normalizedL2SqOnSet (HCPolySupport.openCubeSet Q) (HCPolySupport.Book.Ch03.boundaryForcedCaccioppoliCorrectorOpenH10 rho).toFun ≤ K * (t.rpow (-3) * (HCPolySupport.Book.Ch02.lambdaSq Q t (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a).rpow (-1) * HCPolySupport.Book.Ch03.scaleNormalizedPositiveBesovVectorSeminormTwo Q (2 * t) g) ^ 2

The parent-L² bridge, with the ellipticity constants left in place.

  3^{-2m} ‖ρ‖²_{L²(Q)} ≤ K ( t^{-3} λ_{t,2}^{-1} [g]_{B^{2t}(Q)} )² .

Compare CoarseGraining's internal bridge, which continues to t^{-8} λ_{t,1}^{-1}; see the module docstring.