PenalizationInterior

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

Uniform interior estimate for the penalized resolvents

Inside the part domain the penalization potential vanishes, so the penalized resolvent solves α u_n − ∇·(a∇u_n) = f there with no zeroth-order term. The energy bound ‖u_n‖ ≤ (min α lam)⁻¹ ‖f‖ and the essential bound 2 M on the scalar source are both independent of the penalization index, so the interior Hölder estimate of the small-contrast chain, transported to a Euclidean ball whose double lies inside the part domain, has an index-free constant.

The constant is penalizationInteriorHolderConstant. Nothing is asserted on the boundary of the part domain.

theorem DivergenceFormProcess.Form.euclideanHolderBoundOn_mono {d : ℕ} {W : Set (HCPolySupport.Vec d)} {alpha K K' : ℝ} {v : HCPolySupport.Vec d → ℝ} (hKK : K ≤ K') (h : Algsuperdiff.StochasticProcess.Common.Regularity.Ported.EuclideanHolderBoundOn W alpha K v) : Algsuperdiff.StochasticProcess.Common.Regularity.Ported.EuclideanHolderBoundOn W alpha K' v

A Hölder bound is preserved when the constant is enlarged.

theorem DivergenceFormProcess.Form.continuousOn_of_euclideanHolderBoundOn {d : ℕ} {W : Set (HCPolySupport.Vec d)} {alpha K : ℝ} (halpha : 0 < alpha) {v : HCPolySupport.Vec d → ℝ} (h : Algsuperdiff.StochasticProcess.Common.Regularity.Ported.EuclideanHolderBoundOn W alpha K v) : ContinuousOn v W

A Hölder bound with a positive exponent forces continuity.

theorem DivergenceFormProcess.Form.euclideanHolderBoundOn_iInf {d : ℕ} {W : Set (HCPolySupport.Vec d)} {alpha K : ℝ} {rep : ℕ → HCPolySupport.Vec d → ℝ} (hbdd : ∀ x ∈ W, BddBelow (Set.range fun (n : ℕ) => rep n x)) (h : ∀ (n : ℕ), Algsuperdiff.StochasticProcess.Common.Regularity.Ported.EuclideanHolderBoundOn W alpha K (rep n)) : Algsuperdiff.StochasticProcess.Common.Regularity.Ported.EuclideanHolderBoundOn W alpha K fun (x : HCPolySupport.Vec d) => ⨅ (n : ℕ), rep n x

A common Hölder bound on a pointwise decreasing family is inherited by its pointwise infimum.

theorem DivergenceFormProcess.Form.ZeroTraceSobolev.norm_gradient_le {d : ℕ} {U : Set (HCPolySupport.Vec d)} (u : ZeroTraceSobolev U) : ‖gradient u‖ ≤ ‖u‖

The gradient part of the zero-trace norm.

theorem DivergenceFormProcess.Form.vectorLpSizeOn_grad_le_norm_gradToHilbertVectorL2 {d : ℕ} {U W : Set (HCPolySupport.Vec d)} (hWU : W ⊆ U) (w : HCPolySupport.H1Function U) : Algsuperdiff.StochasticProcess.Common.Regularity.Ported.vectorLpSizeOn W 2 w.grad ≤ ‖w.gradToHilbertVectorL2‖

The Euclidean L² size of the gradient on a subset of the domain is bounded by the norm of its Hilbert-vector L² realization.

noncomputable def DivergenceFormProcess.Form.penalizationInteriorHolderConstant (d : ℕ) (alpha r G M : ℝ) : ℝ

The index-free interior Hölder constant of the penalized resolvents on a ball of radius r whose double lies inside the part domain. It depends on the data only through the gradient budget G and the essential bound M on the forcing.

Equations

• One or more equations did not get rendered due to their size.

theorem DivergenceFormProcess.Form.exists_interior_equation_penalized_with_gradient {d : ℕ} {V U : Set (HCPolySupport.Vec d)} (a : HCPolySupport.CoeffField d) (hU : HCPolySupport.IsOpenBoundedConvexDomain U) (hV : IsOpen V) (hVU : V ⊆ U) {α lam Lam : ℝ} (hα : 0 < α) (hlam : 0 < lam) (hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a) (f : ↥(HCPolySupport.ScalarL2 U)) {M : ℝ} (hM : 0 ≤ M) (hfM : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, |↑↑f x| ≤ M) (n : ℕ) {W : Set (HCPolySupport.Vec d)} (hW : IsOpen W) (hWV : W ⊆ V) : ∃ (z : HCPolySupport.H1Function W) (g : HCPolySupport.Vec d → ℝ), z.toFun =ᵐ[MeasureTheory.volume.restrict W] ↑↑((penalizedResolvent a ⋯ hV hα hlam hEll n) f) ∧ Algsuperdiff.StochasticProcess.Common.Regularity.Ported.MemScalarLInfOn W g ∧ Algsuperdiff.StochasticProcess.Common.Regularity.Ported.scalarLInfSizeOn W g ≤ 2 * M ∧ Algsuperdiff.StochasticProcess.Common.Regularity.Ported.vectorLpSizeOn W 2 z.grad ≤ (min α lam)⁻¹ * ‖f‖ ∧ Algsuperdiff.StochasticProcess.Common.Regularity.Ported.IsMatrixDivFormWeakSolutionZerothOrderOn a W z g 0

The interior equation for the penalized problem together with the index-free bounds on its data.