Coarse-graining support: Support.CoarseGraining.Symmetric.VariationalProblems #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Dirichlet and Neumann predicates for the symmetric split #
This file introduces the PDE-facing predicates used to state the Dirichlet-Neumann interpretation of the symmetric coarse-graining identities. Existence and variational minimality are intentionally left to later files; the predicates here record the boundary conditions and harmonicity in the existing Sobolev/solenoidal language.
def
HCPolySupport.IsAffineDirichletSolution
{d : ℕ}
(a : CoeffField d)
(U : Set (Vec d))
(p : Vec d)
(u : H1Function U)
:
Affine Dirichlet solution with slope p: the gradient is a-harmonic and
differs from the constant gradient p by a zero-trace potential gradient.
Equations
- HCPolySupport.IsAffineDirichletSolution a U p u = (HCPolySupport.IsAHarmonicGradient a U u.grad ∧ HCPolySupport.IsPotentialZeroTraceOn U fun (x : HCPolySupport.Vec d) => u.grad x - p)
Instances For
theorem
HCPolySupport.IsAffineDirichletSolution.isAHarmonicGradient
{d : ℕ}
{a : CoeffField d}
{U : Set (Vec d)}
{p : Vec d}
{u : H1Function U}
(hu : IsAffineDirichletSolution a U p u)
:
IsAHarmonicGradient a U u.grad
theorem
HCPolySupport.IsAffineDirichletSolution.isPotentialZeroTraceOn_grad_sub_const
{d : ℕ}
{a : CoeffField d}
{U : Set (Vec d)}
{p : Vec d}
{u : H1Function U}
(hu : IsAffineDirichletSolution a U p u)
:
IsPotentialZeroTraceOn U fun (x : Vec d) => u.grad x - p
theorem
HCPolySupport.IsAffineDirichletSolution.averageGradient_eq
{d : ℕ}
{a : CoeffField d}
{U : Set (Vec d)}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
{p : Vec d}
{u : H1Function U}
(hu : IsAffineDirichletSolution a U p u)
(hvol : (MeasureTheory.volume U).toReal ≠ 0)
:
def
HCPolySupport.IsAffineDirichletSolution.toAHarmonicFunction
{d : ℕ}
{a : CoeffField d}
{U : Set (Vec d)}
{p : Vec d}
{u : H1Function U}
(hu : IsAffineDirichletSolution a U p u)
:
Forget the affine boundary condition and retain the associated
a-harmonic function.
Equations
- hu.toAHarmonicFunction = { toH1 := u, isHarmonic := ⋯ }
Instances For
@[simp]
theorem
HCPolySupport.IsAffineDirichletSolution.toAHarmonicFunction_toH1
{d : ℕ}
{a : CoeffField d}
{U : Set (Vec d)}
{p : Vec d}
{u : H1Function U}
(hu : IsAffineDirichletSolution a U p u)
:
@[simp]
theorem
HCPolySupport.IsAffineDirichletSolution.toAHarmonicFunction_grad
{d : ℕ}
{a : CoeffField d}
{U : Set (Vec d)}
{p : Vec d}
{u : H1Function U}
(hu : IsAffineDirichletSolution a U p u)
:
theorem
HCPolySupport.IsAffineDirichletSolution.firstVariation_integral_eq_zero_of_isSymmetricCoeffField
{d : ℕ}
{a : CoeffField d}
{U : Set (Vec d)}
{p : Vec d}
{u : H1Function U}
(hu : IsAffineDirichletSolution a U p u)
(ha : IsSymmetricCoeffField a)
(w : AHarmonicFunction a U)
:
theorem
HCPolySupport.IsAffineDirichletSolution.isResponseMaximizer_of_isSymmetricCoeffField_of_isEllipticFieldOn
{d : ℕ}
{a : CoeffField d}
{U : Set (Vec d)}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
{p : Vec d}
{u : H1Function U}
(hu : IsAffineDirichletSolution a U p u)
(ha : IsSymmetricCoeffField a)
{lam Lam : ℝ}
(hEll : IsEllipticFieldOn lam Lam U a)
:
IsResponseMaximizer U (-p) 0 a hu.toAHarmonicFunction
theorem
HCPolySupport.IsAffineDirichletSolution.averageFlux_eq_sigmaCoarse_mul_of_isResponseMaximizer
{d : ℕ}
{a : CoeffField d}
{U : Set (Vec d)}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
{p : Vec d}
{u : H1Function U}
(hu : IsAffineDirichletSolution a U p u)
(hmax : IsResponseMaximizer U (-p) 0 a hu.toAHarmonicFunction)
(ha : IsSymmetricCoeffField a)
(hA : IsCoarseBlockMatrix U a (deterministicCoarseBlockMatrix U a))
{sigma sigmaStar kappa : Mat d}
(hS : IsSigmaStarCoarse U a sigmaStar)
(hK : IsKappaCoarse U a sigmaStar kappa)
(hSigma : IsSigmaCoarse U a sigma sigmaStar kappa)
(hdet : IsUnit (Matrix.det sigmaStar))
(hInt : ResponseLinearIntegrabilityData U a)
(vFlux : (i : Fin d) → ScalarCanonicalMaximizer U (Pi.single i 1) 0 a)
:
theorem
HCPolySupport.IsAffineDirichletSolution.averageFlux_eq_sigmaCoarse_mul_of_isSymmetricCoeffField_of_isEllipticFieldOn
{d : ℕ}
{a : CoeffField d}
{U : Set (Vec d)}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
{p : Vec d}
{u : H1Function U}
(hu : IsAffineDirichletSolution a U p u)
(ha : IsSymmetricCoeffField a)
{lam Lam : ℝ}
(hEll : IsEllipticFieldOn lam Lam U a)
(hA : IsCoarseBlockMatrix U a (deterministicCoarseBlockMatrix U a))
{sigma sigmaStar kappa : Mat d}
(hS : IsSigmaStarCoarse U a sigmaStar)
(hK : IsKappaCoarse U a sigmaStar kappa)
(hSigma : IsSigmaCoarse U a sigma sigmaStar kappa)
(hdet : IsUnit (Matrix.det sigmaStar))
(hInt : ResponseLinearIntegrabilityData U a)
(vFlux : (i : Fin d) → ScalarCanonicalMaximizer U (Pi.single i 1) 0 a)
:
theorem
HCPolySupport.IsAffineDirichletSolution.energy_eq_vecDot_sigmaCoarse_of_isSymmetricCoeffField_of_isEllipticFieldOn
{d : ℕ}
{a : CoeffField d}
{U : Set (Vec d)}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
{p : Vec d}
{u : H1Function U}
(hu : IsAffineDirichletSolution a U p u)
(ha : IsSymmetricCoeffField a)
{lam Lam : ℝ}
(hEll : IsEllipticFieldOn lam Lam U a)
(hA : IsCoarseBlockMatrix U a (deterministicCoarseBlockMatrix U a))
{sigma sigmaStar kappa : Mat d}
(hS : IsSigmaStarCoarse U a sigmaStar)
(hK : IsKappaCoarse U a sigmaStar kappa)
(hSigma : IsSigmaCoarse U a sigma sigmaStar kappa)
(hdet : IsUnit (Matrix.det sigmaStar))
:
volumeAverage U (scalarVariationEnergyIntegrand a hu.toAHarmonicFunction) = vecDot p (matVecMul (sigmaCoarse U a) p)
def
HCPolySupport.IsConstantFluxNeumannSolution
{d : ℕ}
(a : CoeffField d)
(U : Set (Vec d))
(q : Vec d)
(u : H1MeanZeroFunction U)
:
Mean-zero Neumann solution with constant flux q: the function is
a-harmonic and its excess flux a ∇u - q has zero normal trace.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
HCPolySupport.IsConstantFluxNeumannSolution.isAHarmonicGradient
{d : ℕ}
{a : CoeffField d}
{U : Set (Vec d)}
{q : Vec d}
{u : H1MeanZeroFunction U}
(hu : IsConstantFluxNeumannSolution a U q u)
:
theorem
HCPolySupport.IsConstantFluxNeumannSolution.isSolenoidalZeroNormalTraceOn_flux_sub_const
{d : ℕ}
{a : CoeffField d}
{U : Set (Vec d)}
{q : Vec d}
{u : H1MeanZeroFunction U}
(hu : IsConstantFluxNeumannSolution a U q u)
:
IsSolenoidalZeroNormalTraceOn U fun (x : Vec d) => matVecMul (a x) (u.toH1Function.grad x) - q
theorem
HCPolySupport.IsConstantFluxNeumannSolution.averageFlux_eq
{d : ℕ}
{a : CoeffField d}
{U : Set (Vec d)}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
{q : Vec d}
{u : H1MeanZeroFunction U}
(hu : IsConstantFluxNeumannSolution a U q u)
{lam Lam : ℝ}
(hEll : IsEllipticFieldOn lam Lam U a)
(hU : IsSobolevRegularDomain U)
(hvol : (MeasureTheory.volume U).toReal ≠ 0)
:
def
HCPolySupport.IsConstantFluxNeumannSolution.toAHarmonicFunction
{d : ℕ}
{a : CoeffField d}
{U : Set (Vec d)}
{q : Vec d}
{u : H1MeanZeroFunction U}
(hu : IsConstantFluxNeumannSolution a U q u)
:
Forget the constant-flux boundary condition and retain the associated
a-harmonic function.
Equations
- hu.toAHarmonicFunction = { toH1 := u.toH1Function, isHarmonic := ⋯ }
Instances For
@[simp]
theorem
HCPolySupport.IsConstantFluxNeumannSolution.toAHarmonicFunction_toH1
{d : ℕ}
{a : CoeffField d}
{U : Set (Vec d)}
{q : Vec d}
{u : H1MeanZeroFunction U}
(hu : IsConstantFluxNeumannSolution a U q u)
:
@[simp]
theorem
HCPolySupport.IsConstantFluxNeumannSolution.toAHarmonicFunction_grad
{d : ℕ}
{a : CoeffField d}
{U : Set (Vec d)}
{q : Vec d}
{u : H1MeanZeroFunction U}
(hu : IsConstantFluxNeumannSolution a U q u)
:
theorem
HCPolySupport.IsConstantFluxNeumannSolution.firstVariation_integral_eq_zero_of_isSymmetricCoeffField
{d : ℕ}
{a : CoeffField d}
{U : Set (Vec d)}
{q : Vec d}
{u : H1MeanZeroFunction U}
(hu : IsConstantFluxNeumannSolution a U q u)
(ha : IsSymmetricCoeffField a)
(w : AHarmonicFunction a U)
:
theorem
HCPolySupport.IsConstantFluxNeumannSolution.isResponseMaximizer_of_isSymmetricCoeffField_of_isEllipticFieldOn
{d : ℕ}
{a : CoeffField d}
{U : Set (Vec d)}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
{q : Vec d}
{u : H1MeanZeroFunction U}
(hu : IsConstantFluxNeumannSolution a U q u)
(ha : IsSymmetricCoeffField a)
{lam Lam : ℝ}
(hEll : IsEllipticFieldOn lam Lam U a)
:
IsResponseMaximizer U 0 q a hu.toAHarmonicFunction
theorem
HCPolySupport.IsConstantFluxNeumannSolution.averageGradient_eq_sigmaStarInvCoarse_mul_of_isResponseMaximizer
{d : ℕ}
{a : CoeffField d}
{U : Set (Vec d)}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
{q : Vec d}
{u : H1MeanZeroFunction U}
(hu : IsConstantFluxNeumannSolution a U q u)
(hmax : IsResponseMaximizer U 0 q a hu.toAHarmonicFunction)
(ha : IsSymmetricCoeffField a)
(hA : IsCoarseBlockMatrix U a (deterministicCoarseBlockMatrix U a))
{sigmaStar kappa : Mat d}
(hS : IsSigmaStarCoarse U a sigmaStar)
(hK : IsKappaCoarse U a sigmaStar kappa)
(hdet : IsUnit (Matrix.det sigmaStar))
(hInt : ResponseLinearIntegrabilityData U a)
(vGrad : (i : Fin d) → ScalarCanonicalMaximizer U 0 (Pi.single i 1) a)
:
theorem
HCPolySupport.IsConstantFluxNeumannSolution.averageGradient_eq_sigmaStarInvCoarse_mul_of_isSymmetricCoeffField_of_isEllipticFieldOn
{d : ℕ}
{a : CoeffField d}
{U : Set (Vec d)}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
{q : Vec d}
{u : H1MeanZeroFunction U}
(hu : IsConstantFluxNeumannSolution a U q u)
(ha : IsSymmetricCoeffField a)
{lam Lam : ℝ}
(hEll : IsEllipticFieldOn lam Lam U a)
(hA : IsCoarseBlockMatrix U a (deterministicCoarseBlockMatrix U a))
{sigmaStar kappa : Mat d}
(hS : IsSigmaStarCoarse U a sigmaStar)
(hK : IsKappaCoarse U a sigmaStar kappa)
(hdet : IsUnit (Matrix.det sigmaStar))
(hInt : ResponseLinearIntegrabilityData U a)
(vGrad : (i : Fin d) → ScalarCanonicalMaximizer U 0 (Pi.single i 1) a)
:
theorem
HCPolySupport.IsConstantFluxNeumannSolution.energy_eq_vecDot_sigmaStarInvCoarse_of_isSymmetricCoeffField_of_isEllipticFieldOn
{d : ℕ}
{a : CoeffField d}
{U : Set (Vec d)}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
{q : Vec d}
{u : H1MeanZeroFunction U}
(hu : IsConstantFluxNeumannSolution a U q u)
(ha : IsSymmetricCoeffField a)
{lam Lam : ℝ}
(hEll : IsEllipticFieldOn lam Lam U a)
{sigmaStar : Mat d}
(hS : IsSigmaStarCoarse U a sigmaStar)
:
volumeAverage U (scalarVariationEnergyIntegrand a hu.toAHarmonicFunction) = vecDot q (matVecMul (sigmaStarInvCoarse U a) q)
noncomputable def
HCPolySupport.dirichletNeumannSplitOfIsEllipticFieldOn
{d : ℕ}
{a : CoeffField d}
{U : Set (Vec d)}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
{lam Lam : ℝ}
(hEll : IsEllipticFieldOn lam Lam U a)
{p q : Vec d}
{uD : H1Function U}
{uN : H1MeanZeroFunction U}
(huD : IsAffineDirichletSolution a U p uD)
(huN : IsConstantFluxNeumannSolution a U q uN)
:
The harmonic response obtained by subtracting the affine Dirichlet solution
from the constant-flux Neumann solution. This is the Lean object behind the
informal formula v(p,q) = u_q^N - u_p^D in the symmetric case.
Equations
- HCPolySupport.dirichletNeumannSplitOfIsEllipticFieldOn hEll huD huN = huN.toAHarmonicFunction.subOfIntegrable huD.toAHarmonicFunction ⋯ ⋯
Instances For
@[simp]
theorem
HCPolySupport.dirichletNeumannSplitOfIsEllipticFieldOn_grad
{d : ℕ}
{a : CoeffField d}
{U : Set (Vec d)}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
{lam Lam : ℝ}
(hEll : IsEllipticFieldOn lam Lam U a)
{p q : Vec d}
{uD : H1Function U}
{uN : H1MeanZeroFunction U}
(huD : IsAffineDirichletSolution a U p uD)
(huN : IsConstantFluxNeumannSolution a U q uN)
:
theorem
HCPolySupport.isResponseMaximizer_dirichletNeumannSplitOfIsEllipticFieldOn_of_isSymmetricCoeffField
{d : ℕ}
{a : CoeffField d}
{U : Set (Vec d)}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
{lam Lam : ℝ}
(hEll : IsEllipticFieldOn lam Lam U a)
{p q : Vec d}
{uD : H1Function U}
{uN : H1MeanZeroFunction U}
(huD : IsAffineDirichletSolution a U p uD)
(huN : IsConstantFluxNeumannSolution a U q uN)
(ha : IsSymmetricCoeffField a)
:
IsResponseMaximizer U p q a (dirichletNeumannSplitOfIsEllipticFieldOn hEll huD huN)