Stability of shifted weak solutions under coefficient perturbations

This file isolates the Hilbert-space estimate used to prove continuity of a shifted divergence-form solution with respect to its coefficient. The coefficient-specific work is reduced to bounding the difference of the two shifted bilinear forms at one of the solutions.

theorem Algsuperdiff.Section5.Measurability.ShiftedCoefficientContinuity.abs_shiftedBilin_sub_le_of_entry_bound {d : ℕ} {U : Set (HCPolySupport.Vec d)} {a b : HCPolySupport.CoeffField d} {alpha lamA LamA lamB LamB delta : ℝ} (hEllA : HCPolySupport.IsEllipticFieldOn lamA LamA U a) (hEllB : HCPolySupport.IsEllipticFieldOn lamB LamB U b) (hdelta : 0 ≤ delta) (hab : ∀ x ∈ U, ∀ (i j : Fin d), |a x i j - b x i j| ≤ delta) (v w : DivergenceFormProcess.Form.ZeroTraceSobolev U) : |((DivergenceFormProcess.Form.shiftedBilin hEllA alpha) v) w - ((DivergenceFormProcess.Form.shiftedBilin hEllB alpha) v) w| ≤ ↑d * (↑d * delta) * ‖DivergenceFormProcess.Form.ZeroTraceSobolev.gradient v‖ * ‖DivergenceFormProcess.Form.ZeroTraceSobolev.gradient w‖

Difference of shifted bilinear forms controlled by an entrywise coefficient bound. The mass terms cancel, leaving only the coefficient pairing.

theorem Algsuperdiff.Section5.Measurability.ShiftedCoefficientContinuity.norm_alphaShiftedSolution_sub_le_of_bilin_diff {d : ℕ} {U : Set (HCPolySupport.Vec d)} {a b : HCPolySupport.CoeffField d} {alpha lamA LamA lamB LamB eps : ℝ} (halpha : 0 < alpha) (hlamA : 0 < lamA) (hlamB : 0 < lamB) (hEllA : HCPolySupport.IsEllipticFieldOn lamA LamA U a) (hEllB : HCPolySupport.IsEllipticFieldOn lamB LamB U b) (f : ↥(HCPolySupport.ScalarL2 U)) (hpert : ∀ (w : DivergenceFormProcess.Form.ZeroTraceSobolev U), |((DivergenceFormProcess.Form.shiftedBilin hEllA alpha) ((DivergenceFormProcess.Form.alphaShiftedSolution b halpha hlamB hEllB) f)) w - ((DivergenceFormProcess.Form.shiftedBilin hEllB alpha) ((DivergenceFormProcess.Form.alphaShiftedSolution b halpha hlamB hEllB) f)) w| ≤ eps * ‖w‖) (heps : 0 ≤ eps) : ‖(DivergenceFormProcess.Form.alphaShiftedSolution a halpha hlamA hEllA) f - (DivergenceFormProcess.Form.alphaShiftedSolution b halpha hlamB hEllB) f‖ ≤ (min alpha lamA)⁻¹ * eps

Stability of the canonical shifted weak solution under a perturbation of the shifted bilinear form. The coercivity constant is that of the first coefficient.

theorem Algsuperdiff.Section5.Measurability.ShiftedCoefficientContinuity.norm_alphaShiftedResolvent_sub_le_of_bilin_diff {d : ℕ} {U : Set (HCPolySupport.Vec d)} {a b : HCPolySupport.CoeffField d} {alpha lamA LamA lamB LamB eps : ℝ} (halpha : 0 < alpha) (hlamA : 0 < lamA) (hlamB : 0 < lamB) (hEllA : HCPolySupport.IsEllipticFieldOn lamA LamA U a) (hEllB : HCPolySupport.IsEllipticFieldOn lamB LamB U b) (f : ↥(HCPolySupport.ScalarL2 U)) (hpert : ∀ (w : DivergenceFormProcess.Form.ZeroTraceSobolev U), |((DivergenceFormProcess.Form.shiftedBilin hEllA alpha) ((DivergenceFormProcess.Form.alphaShiftedSolution b halpha hlamB hEllB) f)) w - ((DivergenceFormProcess.Form.shiftedBilin hEllB alpha) ((DivergenceFormProcess.Form.alphaShiftedSolution b halpha hlamB hEllB) f)) w| ≤ eps * ‖w‖) (heps : 0 ≤ eps) : ‖(DivergenceFormProcess.Form.alphaShiftedResolvent a halpha hlamA hEllA) f - (DivergenceFormProcess.Form.alphaShiftedResolvent b halpha hlamB hEllB) f‖ ≤ (min alpha lamA)⁻¹ * eps

The corresponding stability estimate for the L² resolvent values.

theorem Algsuperdiff.Section5.Measurability.ShiftedCoefficientContinuity.norm_alphaShiftedSolution_sub_le_of_entry_bound {d : ℕ} {U : Set (HCPolySupport.Vec d)} {a b : HCPolySupport.CoeffField d} {alpha nu LamA LamB delta : ℝ} (halpha : 0 < alpha) (hnu : 0 < nu) (hEllA : HCPolySupport.IsEllipticFieldOn nu LamA U a) (hEllB : HCPolySupport.IsEllipticFieldOn nu LamB U b) (hdelta : 0 ≤ delta) (hab : ∀ x ∈ U, ∀ (i j : Fin d), |a x i j - b x i j| ≤ delta) (f : ↥(HCPolySupport.ScalarL2 U)) : ‖(DivergenceFormProcess.Form.alphaShiftedSolution a halpha hnu hEllA) f - (DivergenceFormProcess.Form.alphaShiftedSolution b halpha hnu hEllB) f‖ ≤ (min alpha nu)⁻¹ * (↑d * (↑d * delta) * ‖DivergenceFormProcess.Form.ZeroTraceSobolev.gradient ((DivergenceFormProcess.Form.alphaShiftedSolution b halpha hnu hEllB) f)‖)

Quantitative stability under a uniform entrywise coefficient perturbation. The solution on the right is fixed, so this estimate is directly suited to a continuity proof at a specified coefficient.

theorem Algsuperdiff.Section5.Measurability.ShiftedCoefficientContinuity.norm_alphaShiftedResolvent_sub_le_of_entry_bound {d : ℕ} {U : Set (HCPolySupport.Vec d)} {a b : HCPolySupport.CoeffField d} {alpha nu LamA LamB delta : ℝ} (halpha : 0 < alpha) (hnu : 0 < nu) (hEllA : HCPolySupport.IsEllipticFieldOn nu LamA U a) (hEllB : HCPolySupport.IsEllipticFieldOn nu LamB U b) (hdelta : 0 ≤ delta) (hab : ∀ x ∈ U, ∀ (i j : Fin d), |a x i j - b x i j| ≤ delta) (f : ↥(HCPolySupport.ScalarL2 U)) : ‖(DivergenceFormProcess.Form.alphaShiftedResolvent a halpha hnu hEllA) f - (DivergenceFormProcess.Form.alphaShiftedResolvent b halpha hnu hEllB) f‖ ≤ (min alpha nu)⁻¹ * (↑d * (↑d * delta) * ‖DivergenceFormProcess.Form.ZeroTraceSobolev.gradient ((DivergenceFormProcess.Form.alphaShiftedSolution b halpha hnu hEllB) f)‖)

The L² resolvent version of the entrywise perturbation estimate.

Canonical shifted solutions over an interior domain

noncomputable def Algsuperdiff.Section5.Measurability.ShiftedCoefficientContinuity.shiftedFieldUpper {d : ℕ} {n : ℤ} {nu : ℝ} (hnu : 0 < nu) (A : ↑(Support.ellipticCube nu 0 n)) : ℝ

An upper ellipticity constant selected for the extension of a compact-cube coefficient, restricted to an interior domain.

Equations

• Algsuperdiff.Section5.Measurability.ShiftedCoefficientContinuity.shiftedFieldUpper hnu A = ⋯.choose

theorem Algsuperdiff.Section5.Measurability.ShiftedCoefficientContinuity.shiftedFieldEllipticity {d : ℕ} {U : Set (HCPolySupport.Vec d)} {n : ℤ} {nu : ℝ} (hnu : 0 < nu) (hU : MeasurableSet U) (hUsub : U ⊆ Support.cubeSetAt 0 n) (A : ↑(Support.ellipticCube nu 0 n)) : HCPolySupport.IsEllipticFieldOn nu (shiftedFieldUpper hnu A) U (Support.extendCoeff 0 n ↑A)

The selected ellipticity certificate on an arbitrary measurable subset of the open cube.

noncomputable def Algsuperdiff.Section5.Measurability.ShiftedCoefficientContinuity.shiftedFieldSolution {d : ℕ} {U : Set (HCPolySupport.Vec d)} {n : ℤ} {nu alpha : ℝ} (hnu : 0 < nu) (halpha : 0 < alpha) (hU : MeasurableSet U) (hUsub : U ⊆ Support.cubeSetAt 0 n) (f : ↥(HCPolySupport.ScalarL2 U)) (A : ↑(Support.ellipticCube nu 0 n)) : DivergenceFormProcess.Form.ZeroTraceSobolev U

Canonical shifted weak solution for a compact-cube coefficient, on an interior measurable domain.

Equations

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

noncomputable def Algsuperdiff.Section5.Measurability.ShiftedCoefficientContinuity.shiftedFieldResolvent {d : ℕ} {U : Set (HCPolySupport.Vec d)} {n : ℤ} {nu alpha : ℝ} (hnu : 0 < nu) (halpha : 0 < alpha) (hU : MeasurableSet U) (hUsub : U ⊆ Support.cubeSetAt 0 n) (f : ↥(HCPolySupport.ScalarL2 U)) (A : ↑(Support.ellipticCube nu 0 n)) : ↥(HCPolySupport.ScalarL2 U)

The associated L² resolvent.

Equations

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

theorem Algsuperdiff.Section5.Measurability.ShiftedCoefficientContinuity.continuous_shiftedFieldResolvent {d : ℕ} {U : Set (HCPolySupport.Vec d)} {n : ℤ} {nu alpha : ℝ} (hnu : 0 < nu) (halpha : 0 < alpha) (hU : MeasurableSet U) (hUsub : U ⊆ Support.cubeSetAt 0 n) (f : ↥(HCPolySupport.ScalarL2 U)) : Continuous (shiftedFieldResolvent hnu halpha hU hUsub f)

The compact parameter-to-resolvent map is continuous in L².

theorem Algsuperdiff.Section5.Measurability.ShiftedCoefficientContinuity.alphaShiftedResolvent_eq_shiftedFieldResolvent_of_eqOn {d : ℕ} {U : Set (HCPolySupport.Vec d)} {n : ℤ} {nu alpha : ℝ} {a : HCPolySupport.CoeffField d} {Lam : ℝ} (hnu : 0 < nu) (halpha : 0 < alpha) (hU : MeasurableSet U) (hUsub : U ⊆ Support.cubeSetAt 0 n) (A : ↑(Support.ellipticCube nu 0 n)) (hEll : HCPolySupport.IsEllipticFieldOn nu Lam U a) (ha : ∀ x ∈ U, a x = Support.extendCoeff 0 n (↑A) x) (f : ↥(HCPolySupport.ScalarL2 U)) : (DivergenceFormProcess.Form.alphaShiftedResolvent a halpha hnu hEll) f = shiftedFieldResolvent hnu halpha hU hUsub f A

Identifying the compact-parameter resolvent with any elliptic coefficient that agrees with its extension on the solution domain.

noncomputable def Algsuperdiff.Section5.Measurability.ShiftedCoefficientContinuity.shiftedFieldSetIntegral {d : ℕ} {U : Set (HCPolySupport.Vec d)} {n : ℤ} {nu alpha : ℝ} (hnu : 0 < nu) (halpha : 0 < alpha) (hU : MeasurableSet U) (hUsub : U ⊆ Support.cubeSetAt 0 n) (f : ↥(HCPolySupport.ScalarL2 U)) (B : Set (HCPolySupport.Vec d)) (A : ↑(Support.ellipticCube nu 0 n)) : ℝ

Integral of the canonical shifted resolvent over a measurable subset.

Equations

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

theorem Algsuperdiff.Section5.Measurability.ShiftedCoefficientContinuity.continuous_shiftedFieldSetIntegral {d : ℕ} {U : Set (HCPolySupport.Vec d)} {n : ℤ} {nu alpha : ℝ} (hnu : 0 < nu) (halpha : 0 < alpha) (hU : MeasurableSet U) (hUfin : MeasureTheory.volume U ≠ ⊤) (hUsub : U ⊆ Support.cubeSetAt 0 n) (f : ↥(HCPolySupport.ScalarL2 U)) {B : Set (HCPolySupport.Vec d)} (hBsub : B ⊆ U) : Continuous (shiftedFieldSetIntegral hnu halpha hU hUsub f B)

Set integrals of the shifted resolvent vary continuously with the compact coefficient.