EllipticityWitness

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

Independence from ellipticity witnesses

The canonical weak solution is independent of the quantitative ellipticity certificate used to construct it. These lemmas let an exhaustion use the compactness-supplied upper constant of each domain without changing the represented operator.

theorem DivergenceFormProcess.Form.alphaShiftedSolution_eq_of_ellipticityWitness {d : ℕ} {U : Set (HCPolySupport.Vec d)} (a : HCPolySupport.CoeffField d) {alpha lam₁ Lam₁ lam₂ Lam₂ : ℝ} (halpha : 0 < alpha) (hlam₁ : 0 < lam₁) (hlam₂ : 0 < lam₂) (hEll₁ : HCPolySupport.IsEllipticFieldOn lam₁ Lam₁ U a) (hEll₂ : HCPolySupport.IsEllipticFieldOn lam₂ Lam₂ U a) (f : ↥(HCPolySupport.ScalarL2 U)) : (alphaShiftedSolution a halpha hlam₁ hEll₁) f = (alphaShiftedSolution a halpha hlam₂ hEll₂) f

Alpha-shifted solutions built from two valid ellipticity certificates are equal, because both solve the same weak equation.

theorem DivergenceFormProcess.Form.potentialSolution_eq_of_ellipticityWitness {d : ℕ} {U : Set (HCPolySupport.Vec d)} (a : HCPolySupport.CoeffField d) {alpha lam₁ Lam₁ lam₂ Lam₂ C₁ C₂ : ℝ} (halpha : 0 < alpha) (hlam₁ : 0 < lam₁) (hlam₂ : 0 < lam₂) (hEll₁ : HCPolySupport.IsEllipticFieldOn lam₁ Lam₁ U a) (hEll₂ : HCPolySupport.IsEllipticFieldOn lam₂ Lam₂ U a) (q : HCPolySupport.Vec d → ℝ) (hq₁ : IsBoundedNonnegativePotential U q C₁) (hq₂ : IsBoundedNonnegativePotential U q C₂) (f : ↥(HCPolySupport.ScalarL2 U)) : (potentialSolution a halpha hlam₁ hEll₁ q hq₁) f = (potentialSolution a halpha hlam₂ hEll₂ q hq₂) f

Potential solutions built from two valid ellipticity certificates are equal, because both solve the same weak equation with potential.

theorem DivergenceFormProcess.Form.potentialResolvent_eq_of_ellipticityWitness {d : ℕ} {U : Set (HCPolySupport.Vec d)} (a : HCPolySupport.CoeffField d) {alpha lam₁ Lam₁ lam₂ Lam₂ C₁ C₂ : ℝ} (halpha : 0 < alpha) (hlam₁ : 0 < lam₁) (hlam₂ : 0 < lam₂) (hEll₁ : HCPolySupport.IsEllipticFieldOn lam₁ Lam₁ U a) (hEll₂ : HCPolySupport.IsEllipticFieldOn lam₂ Lam₂ U a) (q : HCPolySupport.Vec d → ℝ) (hq₁ : IsBoundedNonnegativePotential U q C₁) (hq₂ : IsBoundedNonnegativePotential U q C₂) : potentialResolvent a halpha hlam₁ hEll₁ q hq₁ = potentialResolvent a halpha hlam₂ hEll₂ q hq₂

Potential resolvents do not depend on the ellipticity certificate used in their Lax–Milgram construction.

theorem DivergenceFormProcess.Form.potentialSolution_eq_of_ae_eq_potential {d : ℕ} {U : Set (HCPolySupport.Vec d)} (a : HCPolySupport.CoeffField d) {alpha lam Lam C₁ C₂ : ℝ} (halpha : 0 < alpha) (hlam : 0 < lam) (hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a) (q₁ q₂ : HCPolySupport.Vec d → ℝ) (hq₁ : IsBoundedNonnegativePotential U q₁ C₁) (hq₂ : IsBoundedNonnegativePotential U q₂ C₂) (hqeq : q₁ =ᵐ[HCPolySupport.volumeMeasureOn U] q₂) (f : ↥(HCPolySupport.ScalarL2 U)) : (potentialSolution a halpha hlam hEll q₁ hq₁) f = (potentialSolution a halpha hlam hEll q₂ hq₂) f

Potential solutions depend only on the almost-everywhere value of the potential on the domain.

theorem DivergenceFormProcess.Form.potentialResolvent_eq_of_ae_eq_potential {d : ℕ} {U : Set (HCPolySupport.Vec d)} (a : HCPolySupport.CoeffField d) {alpha lam Lam C₁ C₂ : ℝ} (halpha : 0 < alpha) (hlam : 0 < lam) (hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a) (q₁ q₂ : HCPolySupport.Vec d → ℝ) (hq₁ : IsBoundedNonnegativePotential U q₁ C₁) (hq₂ : IsBoundedNonnegativePotential U q₂ C₂) (hqeq : q₁ =ᵐ[HCPolySupport.volumeMeasureOn U] q₂) : potentialResolvent a halpha hlam hEll q₁ hq₁ = potentialResolvent a halpha hlam hEll q₂ hq₂

Potential resolvents are unchanged when the potential is modified on a null subset of the domain.