Cutoff reduction of a local weak solution to an H₀¹ problem #
Evans, Partial Differential Equations (2nd ed.), §6.3.1, Theorem 1, step 1 tests the equation
against -D_k^{-h}(ζ² D_k^h u), which is admissible for u ∈ H¹(U) because the cutoff ζ
removes the boundary. This file uses the same cutoff differently: for a local weak solution
U ∈ W12 Ω and a test function η of Ω, the product η U lies in H₀¹(Ω)
(cutoffMul_mem_H01_of_mem_W12) and solves B[η U, w] = ∫ F w for every w ∈ H₀¹(Ω), with
F = η f − Σ a_{ij} ∂_j η U_i − Σ ∂_j a_{ij} ∂_i η U_0 − Σ a_{ij} ∂_i η U_j
− Σ a_{ij} ∂_{ij} η U_0 + Σ b_i ∂_i η U_0.
Every term of F is in L²(Ω) with a bound in ‖f‖ and ‖U‖, so the interior chain for
H₀¹ solutions applies to η U unchanged, and η = 1 near the set of interest makes the
cutoff invisible in its conclusion.
The derivative ∂_j a_{ij} enters through one integration by parts, the only place a derivative
of a coefficient appears. CoeffWeakGrad records what that step needs: a weak partial derivative
of each entry, measurable and essentially bounded. Both a C¹ bundle
(IsC1Coeff.coeffWeakGrad) and a W^{k+1,∞} bundle (IsWkInftyCoeff.coeffWeakGrad) supply it,
so one reduction serves the H² estimate and the higher-order induction.
Main declarations #
CoeffWeakGrad,IsC1Coeff.coeffWeakGrad,IsWkInftyCoeff.coeffWeakGrad.principal_leibniz: the integration by parts moving∂_joff the test function.reduction_testFn: the reduced identity against test functions.redDatum,reduction_weakForm: the datum as anL²(Ω)class, and the identity onH₀¹(Ω).
Weak gradient of the principal coefficients. For each direction l and entry (i, j),
a measurable function da l i j, essentially bounded by one constant, that is the weak partial
derivative of a_{ij} in direction l. This is all the cutoff reduction asks of the principal
part beyond FullEllipticOp.
The weak partial derivative
∂_l a_{ij}, indexed asda l i j.- measurable (l i j : Fin d) : Measurable (self.da l i j)
Every derivative is measurable.
- bound : ℝ
The common essential bound.
Every derivative is essentially bounded by
bound.- hasWeakPartial (l i j : Fin d) : HasWeakPartial l (fun (x : EuclideanSpace ℝ (Fin d)) => A.a x i j) (self.da l i j)
da l i jis the weak partial derivative ofa_{ij}in directionl.
Instances For
Pointwise bound on a partial of a C¹ coefficient.
A partial of a C¹ coefficient is measurable, being continuous.
The classical partials of a C¹ coefficient are its weak partials.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The first-order members of a W^{k+1,∞} family are weak partials of the coefficient.
Equations
Instances For
A bounded measurable weight times an L²(Ω) class times a continuous compactly supported
function is integrable on Ω.
Integration by parts on the principal term. The term ∫ a_{ij} U₀ ∂_i η ∂_j v with the
derivative moved off v. It is the only place a derivative of a coefficient enters, and it is
taken in the weak sense through HasWeakDerivOn.mul_isWkInfty_left, so the test function stays
smooth and Ω need not have finite measure.
Cutoff reduction against test functions. For a local weak solution U ∈ W12 Ω and a
test function η of Ω, the element η U ∈ H₀¹(Ω) satisfies B[η U, v] = ∫ F v for every
test function v, with F spelled out as separate integrals.
The datum as an L²(Ω) class #
Multiplication by c · ψ on L²(Ω), for c essentially bounded and ψ continuous with
compact support.
Equations
- EllipticPdes.Regularity.weightL Ω hcm hc hψ hψcs = EllipticPdes.Sobolev.mulCoeffL ⋯ ⋯
Instances For
Reduction datum F for η U, as an L²(Ω) class: each term is a bounded weight
supported in tsupport η against f, U₀ or a gradient coordinate of U.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Cutoff reduction on H₀¹(Ω). For a local weak solution U ∈ W12 Ω and a test function
η of Ω, B[η U, w] = ∫ F w for every w ∈ H₀¹(Ω), with F = redDatum.