ZerothOrderIteration #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Dyadic iteration with a geometrically decaying scalar source #
theorem
Algsuperdiff.StochasticProcess.Common.Regularity.Ported.dyadicSmallContrastIteration_zerothOrder
{A : ℕ → ℝ}
{alpha B C : ℝ}
(halpha0 : 0 < alpha)
(halpha1 : alpha < 1)
(hA : ∀ (n : ℕ), 0 ≤ A n)
(hB : 0 ≤ B)
(hC : 0 ≤ C)
(hrec : ∀ (n : ℕ), A (n + 1) ≤ smallContrastContraction alpha * A n + B + C * (1 / 2) ^ n)
(n : ℕ)
:
A scalar source whose dyadic contribution decays by one half adds only
the literal factor 2, while the divergence source retains the printed
8(1-alpha)⁻¹ factor.
theorem
Algsuperdiff.StochasticProcess.Common.Regularity.Ported.dyadicGradientScaleBound_zerothOrder_on_interiorBall
{d : ℕ}
[NeZero d]
{U : Set (HCPolySupport.Vec d)}
(z : HCPolySupport.Vec d)
{R : ℝ}
(hR : 0 < R)
(hR1 : R ≤ 1)
(houter : HCPolySupport.euclideanBall z R ⊆ U)
{a : HCPolySupport.CoeffField d}
{u : HCPolySupport.H1Function U}
{g : HCPolySupport.Vec d → ℝ}
{f : HCPolySupport.Vec d → HCPolySupport.Vec d}
{delta alpha : ℝ}
(hd : 2 ≤ d)
(halpha0 : 0 < alpha)
(halpha1 : alpha < 1)
(hdelta0 : 0 ≤ delta)
(hdelta : delta ≤ smallContrastThreshold d alpha)
(hUopen : IsOpen U)
(hmeas : Measurable a)
(ha : CoefficientIdentityDistanceLE U a delta)
(hu : IsMatrixDivFormWeakSolutionZerothOrderOn a U u g f)
(hg : MemScalarLInfOn U g)
(hf : MemVectorLpOn U (schauderSourceExponent d alpha) f)
(n : ℕ)
:
smallContrastDyadicRadius R n ^ (1 - alpha) * vectorNormalizedL2On (HCPolySupport.euclideanBall z (smallContrastDyadicRadius R n)) u.grad ≤ R ^ (1 - alpha) * vectorNormalizedL2On (HCPolySupport.euclideanBall z R) u.grad + 16 * (1 - alpha)⁻¹ * ((1 / 2) ^ (-↑d / 2) * smallContrastUnitBallVolumePrice d) * vectorLpSizeOn U (schauderSourceExponent d alpha) f + 8 * (1 / 2) ^ (-↑d / 2) * unitCubeDirichletPoincareExplicit d * ↑d * scalarLInfSizeOn U g
The concrete dyadic estimate on an interior ball for an equation with both
a divergence source and a bounded scalar source. The scalar price is uniform
in alpha.