Coarse-graining support: Support.Internal.Ch02.DoubledResponse.ResponseSpace #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Doubled Response Space #
This file is split mechanically out of Internal.Ch02.DoubledResponse.
theorem
HCPolySupport.Internal.Ch02.BookCh02.potentialFieldOn_of_ae_eq
{d : ℕ}
{U : Set (Vec d)}
{f g : Vec d → Vec d}
(hfg : f =ᵐ[volumeMeasureOn U] g)
(hg : Book.Ch01.PotentialFieldOn U g)
:
theorem
HCPolySupport.Internal.Ch02.BookCh02.solenoidalFieldOn_of_ae_eq
{d : ℕ}
{U : Set (Vec d)}
{f g : Vec d → Vec d}
(hfg : f =ᵐ[volumeMeasureOn U] g)
(hg : Book.Ch01.SolenoidalFieldOn U g)
:
theorem
HCPolySupport.Internal.Ch02.BookCh02.isDoubledResponseField_of_sameAE
{d : ℕ}
(U : Book.Ch02.Domain d)
(a : Book.Ch02.CoeffOn U)
{X Y : Book.Ch02.DoubledField d}
(hXY : X.SameAE Y)
(hY : Book.Ch02.IsDoubledResponseField U a Y)
:
theorem
HCPolySupport.Internal.Ch02.BookCh02.isPotentialOn_congr_ae
{d : ℕ}
{U : Set (Vec d)}
{f g : Vec d → Vec d}
(hfg : f =ᵐ[MeasureTheory.volume.restrict U] g)
(hf : IsPotentialOn U f)
:
IsPotentialOn U g
theorem
HCPolySupport.Internal.Ch02.BookCh02.potentialFieldOn_of_isPotentialOn
{d : ℕ}
{U : Set (Vec d)}
{f : Vec d → Vec d}
(hf : IsPotentialOn U f)
:
theorem
HCPolySupport.Internal.Ch02.BookCh02.isPotentialOn_of_potentialFieldOn
{d : ℕ}
{U : Set (Vec d)}
{f : Vec d → Vec d}
(hf : Book.Ch01.PotentialFieldOn U f)
:
IsPotentialOn U f
theorem
HCPolySupport.Internal.Ch02.BookCh02.isPotentialZeroTraceOn_of_potentialZeroTraceFieldOn
{d : ℕ}
{U : Set (Vec d)}
{f : Vec d → Vec d}
(hf : Book.Ch01.PotentialZeroTraceFieldOn U f)
:
theorem
HCPolySupport.Internal.Ch02.BookCh02.solenoidalFieldOn_of_isSolenoidalOn
{d : ℕ}
{U : Set (Vec d)}
{g : Vec d → Vec d}
(hg_mem : MemVectorL2 U g)
(hg : IsSolenoidalOn U g)
:
theorem
HCPolySupport.Internal.Ch02.BookCh02.lowerImage_memVectorL2_of_memVectorL2_of_isEllipticFieldOn
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
{X : BlockState d}
{lam Lam : ℝ}
(hPot : MemVectorL2 U X.potential)
(hFlux : MemVectorL2 U X.flux)
(hEll : IsEllipticFieldOn lam Lam U a)
:
MemVectorL2 U fun (x : Vec d) => (blockMatVecMul (blockCoeffField a x) (X.eval x)).2
theorem
HCPolySupport.Internal.Ch02.BookCh02.upper_add_flux_eq_matVecMul_potential_add_lowerImage_of_isEllipticFieldOn
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
{lam Lam : ℝ}
{X : BlockState d}
(hEll : IsEllipticFieldOn lam Lam U a)
{x : Vec d}
(hx : x ∈ U)
:
(blockMatVecMul (blockCoeffField a x) (X.eval x)).1 + X.flux x = matVecMul (a x) (X.potential x + (blockMatVecMul (blockCoeffField a x) (X.eval x)).2)
theorem
HCPolySupport.Internal.Ch02.BookCh02.upperImage_memVectorL2_of_memVectorL2_of_isEllipticFieldOn
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
{X : BlockState d}
{lam Lam : ℝ}
(hPot : MemVectorL2 U X.potential)
(hFlux : MemVectorL2 U X.flux)
(hLower : MemVectorL2 U fun (x : Vec d) => (blockMatVecMul (blockCoeffField a x) (X.eval x)).2)
(hEll : IsEllipticFieldOn lam Lam U a)
:
MemVectorL2 U fun (x : Vec d) => (blockMatVecMul (blockCoeffField a x) (X.eval x)).1
theorem
HCPolySupport.Internal.Ch02.BookCh02.blockResponseSpace_of_isDoubledResponseField_of_isEllipticFieldOn
{d : ℕ}
(U : Book.Ch02.Domain d)
(a : Book.Ch02.CoeffOn U)
(hEll : IsEllipticFieldOn a.lam a.Lam U.carrier a.toCoeffField)
{X : Book.Ch02.DoubledField d}
(hX : Book.Ch02.IsDoubledResponseField U a X)
:
theorem
HCPolySupport.Internal.Ch02.BookCh02.isDoubledResponseField_of_blockResponseSpace
{d : ℕ}
(U : Book.Ch02.Domain d)
(a : Book.Ch02.CoeffOn U)
{X : BlockState d}
(hX : BlockResponseSpace a.toCoeffField U.carrier X)
(hFlux : MemVectorL2 U.carrier X.flux)
:
theorem
HCPolySupport.Internal.Ch02.BookCh02.doubledFieldOfSolutions_flux_memL2_of_isEllipticFieldOn
{d : ℕ}
(U : Book.Ch02.Domain d)
(a : Book.Ch02.CoeffOn U)
(hEll : IsEllipticFieldOn a.lam a.Lam U.carrier a.toCoeffField)
(v : Book.Ch02.Solution U a)
(vStar : Book.Ch02.Solution U a.transpose)
:
MemVectorL2 U.carrier (Book.Ch02.doubledFieldOfSolutions a v vStar).flux
theorem
HCPolySupport.Internal.Ch02.BookCh02.doubledFieldOfSolutions_mem_responseField_of_isEllipticFieldOn
{d : ℕ}
(U : Book.Ch02.Domain d)
(a : Book.Ch02.CoeffOn U)
(hEll : IsEllipticFieldOn a.lam a.Lam U.carrier a.toCoeffField)
(v : Book.Ch02.Solution U a)
(vStar : Book.Ch02.Solution U a.transpose)
:
Book.Ch02.IsDoubledResponseField U a (Book.Ch02.doubledFieldOfSolutions a v vStar)
theorem
HCPolySupport.Internal.Ch02.BookCh02.response_space_by_solutions_of_isEllipticFieldOn
{d : ℕ}
(U : Book.Ch02.Domain d)
(a : Book.Ch02.CoeffOn U)
(hEll : IsEllipticFieldOn a.lam a.Lam U.carrier a.toCoeffField)
(X : Book.Ch02.DoubledField d)
:
Book.Ch02.IsDoubledResponseField U a X ↔ ∃ (v : Book.Ch02.Solution U a) (vStar : Book.Ch02.Solution U a.transpose),
X.SameAE (Book.Ch02.doubledFieldOfSolutions a v vStar)
theorem
HCPolySupport.Internal.Ch02.BookCh02.book_doubledResponseValue_eq_blockResponseIntegrand
{d : ℕ}
(U : Book.Ch02.Domain d)
(a : Book.Ch02.CoeffOn U)
(P Q : BlockVec d)
(X : Book.Ch02.DoubledField d)
:
Book.Ch02.doubledResponseValue U a P Q X = volumeAverage U.carrier (blockResponseIntegrand a.toCoeffField P Q (blockStateOfDoubled X))
theorem
HCPolySupport.Internal.Ch02.BookCh02.book_doubledResponseValue_ofBlockState_eq_blockResponseIntegrand
{d : ℕ}
(U : Book.Ch02.Domain d)
(a : Book.Ch02.CoeffOn U)
(P Q : BlockVec d)
(X : BlockState d)
:
Book.Ch02.doubledResponseValue U a P Q (doubledFieldOfBlockState X) = volumeAverage U.carrier (blockResponseIntegrand a.toCoeffField P Q X)
theorem
HCPolySupport.Internal.Ch02.BookCh02.book_doubledResponseValueSet_eq_blockJValueSet_of_isEllipticFieldOn
{d : ℕ}
(U : Book.Ch02.Domain d)
(a : Book.Ch02.CoeffOn U)
(hEll : IsEllipticFieldOn a.lam a.Lam U.carrier a.toCoeffField)
(P Q : BlockVec d)
:
theorem
HCPolySupport.Internal.Ch02.BookCh02.book_doubledResponseJ_eq_BlockJ_of_isEllipticFieldOn
{d : ℕ}
(U : Book.Ch02.Domain d)
(a : Book.Ch02.CoeffOn U)
(hEll : IsEllipticFieldOn a.lam a.Lam U.carrier a.toCoeffField)
(P Q : BlockVec d)
: