Coarse-graining support: Support.CoarseGraining.BlockResponse.Foundations.IntegrabilityFamily #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
BlockResponse Foundations -- integrability data family #
BlockJIntegrabilityData and BlockResponseLowerImageMemVectorL2Data structures, blockResponseIntegrabilityData smul / zero, the flux_memL2 / lowerImage variants from IsEllipticFieldOn, the blockResponseIntegrand_integrableOn theorems, and the BlockJIntegrabilityData.of_lowerImageMemVectorL2Data bridge.
theorem
HCPolySupport.blockEnergyDensity_smul_state
{d : ℕ}
(a : CoeffField d)
(c : ℝ)
(X : BlockState d)
:
theorem
HCPolySupport.BlockResponseIntegrabilityData.smul
{d : ℕ}
{a : CoeffField d}
{U : Set (Vec d)}
{X : BlockState d}
(hInt : BlockResponseIntegrabilityData U a X)
(c : ℝ)
:
BlockResponseIntegrabilityData U a (c • X)
theorem
HCPolySupport.blockResponseIntegrabilityData_zero
{d : ℕ}
(U : Set (Vec d))
(a : CoeffField d)
:
BlockResponseIntegrabilityData U a { potential := 0, flux := 0 }
theorem
HCPolySupport.blockResponseIntegrabilityData_of_flux_memL2_of_mem_responseSpace_of_isEllipticFieldOn
{d : ℕ}
{a : CoeffField d}
{U : Set (Vec d)}
{X : BlockState d}
{lam Lam : ℝ}
(hX : BlockResponseSpace a U X)
(hFlux : MemVectorL2 U X.flux)
(hEll : IsEllipticFieldOn lam Lam U a)
:
theorem
HCPolySupport.blockResponse_lowerImage_memL2_of_flux_memL2_responseSpace
{d : ℕ}
{a : CoeffField d}
{U : Set (Vec d)}
{X : BlockState d}
{lam Lam : ℝ}
(hX : BlockResponseSpace a U X)
(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.blockResponse_flux_memL2_of_lowerImage_memVectorL2_of_mem_responseSpace_of_isEllipticFieldOn
{d : ℕ}
{a : CoeffField d}
{U : Set (Vec d)}
{X : BlockState d}
{lam Lam : ℝ}
(hX : BlockResponseSpace a U X)
(hLowerL2 : MemVectorL2 U fun (x : Vec d) => (blockMatVecMul (blockCoeffField a x) (X.eval x)).2)
(hEll : IsEllipticFieldOn lam Lam U a)
:
MemVectorL2 U X.flux
theorem
HCPolySupport.blockResponse_flux_memL2_of_lowerImage_potential_ae
{d : ℕ}
{a : CoeffField d}
{U : Set (Vec d)}
{X : BlockState d}
{lam Lam : ℝ}
(hX : BlockResponseSpace a U X)
{f : Vec d → Vec d}
(hLowerPot : IsPotentialOn U f)
(hLowerEq : (fun (x : Vec d) => (blockMatVecMul (blockCoeffField a x) (X.eval x)).2) =ᵐ[volumeMeasureOn U] f)
(hEll : IsEllipticFieldOn lam Lam U a)
:
MemVectorL2 U X.flux
theorem
HCPolySupport.blockResponse_flux_memL2_of_lowerImage_isPotential_of_mem_responseSpace_of_isEllipticFieldOn
{d : ℕ}
{a : CoeffField d}
{U : Set (Vec d)}
{X : BlockState d}
{lam Lam : ℝ}
(hX : BlockResponseSpace a U X)
(hLower : IsPotentialOn U fun (x : Vec d) => (blockMatVecMul (blockCoeffField a x) (X.eval x)).2)
(hEll : IsEllipticFieldOn lam Lam U a)
:
MemVectorL2 U X.flux
theorem
HCPolySupport.blockResponseIntegrabilityData_of_ellipticField
{d : ℕ}
{a : CoeffField d}
{U : Set (Vec d)}
{X : BlockState d}
{lam Lam : ℝ}
(hX : BlockResponseSpace a U X)
{f : Vec d → Vec d}
(hLowerPot : IsPotentialOn U f)
(hLowerEq : (fun (x : Vec d) => (blockMatVecMul (blockCoeffField a x) (X.eval x)).2) =ᵐ[volumeMeasureOn U] f)
(hEll : IsEllipticFieldOn lam Lam U a)
:
theorem
HCPolySupport.blockResponseIntegrabilityData_of_lowerImage_isPotential_of_mem_responseSpace_of_isEllipticFieldOn
{d : ℕ}
{a : CoeffField d}
{U : Set (Vec d)}
{X : BlockState d}
{lam Lam : ℝ}
(hX : BlockResponseSpace a U X)
(hLower : IsPotentialOn U fun (x : Vec d) => (blockMatVecMul (blockCoeffField a x) (X.eval x)).2)
(hEll : IsEllipticFieldOn lam Lam U a)
:
theorem
HCPolySupport.blockResponseIntegrabilityData_of_lowerImage_memL2
{d : ℕ}
{a : CoeffField d}
{U : Set (Vec d)}
{X : BlockState d}
{lam Lam : ℝ}
(hX : BlockResponseSpace a U X)
(hLowerL2 : MemVectorL2 U fun (x : Vec d) => (blockMatVecMul (blockCoeffField a x) (X.eval x)).2)
(hEll : IsEllipticFieldOn lam Lam U a)
:
theorem
HCPolySupport.blockResponseIntegrand_integrable_of_integrabilityData
{d : ℕ}
{a : CoeffField d}
{U : Set (Vec d)}
{X : BlockState d}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
{lam Lam : ℝ}
(hX : BlockResponseSpace a U X)
(hInt : BlockResponseIntegrabilityData U a X)
(hEll : IsEllipticFieldOn lam Lam U a)
(P Q : BlockVec d)
:
theorem
HCPolySupport.blockResponseIntegrand_integrableOn_of_lowerImage_memVectorL2
{d : ℕ}
{a : CoeffField d}
{U : Set (Vec d)}
{X : BlockState d}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
{lam Lam : ℝ}
(hX : BlockResponseSpace a U X)
(hLowerL2 : MemVectorL2 U fun (x : Vec d) => (blockMatVecMul (blockCoeffField a x) (X.eval x)).2)
(hEll : IsEllipticFieldOn lam Lam U a)
(P Q : BlockVec d)
:
theorem
HCPolySupport.BlockJIntegrabilityData.of_lowerImageMemVectorL2Data_of_isEllipticFieldOn
{d : ℕ}
{a : CoeffField d}
{U : Set (Vec d)}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
{lam Lam : ℝ}
(hLower : BlockResponseLowerImageMemVectorL2Data U a)
(hEll : IsEllipticFieldOn lam Lam U a)
(P Q : BlockVec d)
:
BlockJIntegrabilityData U a P Q