SolutionLinearity #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The solution map is linear, and representatives subtract #
For a fixed coefficient field the localized Dirichlet problem is linear in the pair (solution, forcing field): the difference of two solutions solves the problem for the difference of the forcing fields. Continuous representatives subtract as well.
This is the linearity input used to compare two localized problems.
References #
- ABK26, the localized Dirichlet problems of Section 5.1.
1. Linearity of the localized Dirichlet problem #
theorem
Algsuperdiff.Section5.Support.isDirichletSolutionAt_sub
{d : ℕ}
{y : HCPolySupport.Vec d}
{n : ℤ}
{a : HCPolySupport.CoeffField d}
{lam Lam : ℝ}
(hEll : HCPolySupport.IsEllipticFieldOn lam Lam (cubeSetAt y n) a)
{u u' : HCPolySupport.H1Function (cubeSetAt y n)}
{g g' : HCPolySupport.Vec d → HCPolySupport.Vec d}
(hgL2 : HCPolySupport.MemVectorL2 (cubeSetAt y n) g)
(hg'L2 : HCPolySupport.MemVectorL2 (cubeSetAt y n) g')
(hu : IsDirichletSolutionAt a y n u g)
(hu' : IsDirichletSolutionAt a y n u' g')
:
IsDirichletSolutionAt a y n (u - u') fun (x : HCPolySupport.Vec d) => g x - g' x
The difference of two solutions solves the problem for the difference of the forcing fields.
2. Representatives subtract #
theorem
Algsuperdiff.Section5.Support.isCubeRepresentative_sub
{d : ℕ}
{y : HCPolySupport.Vec d}
{n : ℤ}
{u u' : HCPolySupport.H1Function (cubeSetAt y n)}
{uRep u'Rep : HCPolySupport.Vec d → ℝ}
(h : IsCubeRepresentative y n u uRep)
(h' : IsCubeRepresentative y n u' u'Rep)
:
IsCubeRepresentative y n (u - u') fun (x : HCPolySupport.Vec d) => uRep x - u'Rep x