Coarse-graining support: Support.CoarseGraining.BlockResponse.Foundations.PairHalfAdmissible #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
BlockResponse Foundations -- pair-half admissibility #
blockResponse_pair_half isBlockMuAdmissible and averagePotential / averageFlux identities: from the basic average-eq hypothesis, under scalarCanonicalMaximizers data (with or without basis data) and under the IsOpenBoundedConvexDomain assumption.
theorem
HCPolySupport.blockResponse_pair_half_averagePotential_eq_zero_of_scalarCanonicalMaximizers_zero_right
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
{sigmaStar kappa : Mat d}
{q : Vec d}
(u : ScalarCanonicalMaximizer U 0 q a)
(v : ScalarCanonicalMaximizer U 0 (-q) (adjointCoeffField a))
(hS : IsSigmaStarCoarse U a sigmaStar)
(hK : IsKappaCoarse U a sigmaStar kappa)
(hSAdj : IsSigmaStarCoarse U (adjointCoeffField a) sigmaStar)
(hKAdj : IsKappaCoarse U (adjointCoeffField a) sigmaStar (-kappa))
(hdet : IsUnit (Matrix.det sigmaStar))
(hInt : ResponseLinearIntegrabilityData U a)
(hIntAdj : ResponseLinearIntegrabilityData U (adjointCoeffField a))
(uGrad : (i : Fin d) → ScalarCanonicalMaximizer U 0 (Pi.single i 1) a)
(vGrad : (i : Fin d) → ScalarCanonicalMaximizer U 0 (Pi.single i 1) (adjointCoeffField a))
:
(fun (i : Fin d) =>
integralAverage U fun (x : Vec d) =>
(blockResponsePairHalfState a u.toAHarmonicFunctionMeanZero.toAHarmonicFunction
v.toAHarmonicFunctionMeanZero.toAHarmonicFunction).potential
x i) = 0
The half-pair witness built from a primal maximizer at (0,q) and an
adjoint maximizer at (0,-q) has zero average potential.
theorem
HCPolySupport.blockResponse_pair_half_averagePotential_eq_zero_of_basisData
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
{sigmaStar kappa : Mat d}
{q : Vec d}
(u : ScalarCanonicalMaximizer U 0 q a)
(v : ScalarCanonicalMaximizer U 0 (-q) (adjointCoeffField a))
(hS : IsSigmaStarCoarse U a sigmaStar)
(hK : IsKappaCoarse U a sigmaStar kappa)
(hSAdj : IsSigmaStarCoarse U (adjointCoeffField a) sigmaStar)
(hKAdj : IsKappaCoarse U (adjointCoeffField a) sigmaStar (-kappa))
(hdet : IsUnit (Matrix.det sigmaStar))
(hInt : ResponseLinearIntegrabilityData U a)
(hIntAdj : ResponseLinearIntegrabilityData U (adjointCoeffField a))
(basisGrad : ScalarCanonicalMaximizer.GradientBasisData U a)
(basisGradAdj : ScalarCanonicalMaximizer.GradientBasisData U (adjointCoeffField a))
:
(fun (i : Fin d) =>
integralAverage U fun (x : Vec d) =>
(blockResponsePairHalfState a u.toAHarmonicFunctionMeanZero.toAHarmonicFunction
v.toAHarmonicFunctionMeanZero.toAHarmonicFunction).potential
x i) = 0
Bundled basis-data wrapper for the previous zero-average-potential identity.
theorem
HCPolySupport.blockResponse_pair_half_averageFlux_eq_of_scalarCanonicalMaximizers_zero_right
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
{sigma sigmaStar kappa : Mat d}
{q : Vec d}
(u : ScalarCanonicalMaximizer U 0 q a)
(v : ScalarCanonicalMaximizer U 0 (-q) (adjointCoeffField a))
(hS : IsSigmaStarCoarse U a sigmaStar)
(hK : IsKappaCoarse U a sigmaStar kappa)
(hSigma : IsSigmaCoarse U a sigma sigmaStar kappa)
(hSAdj : IsSigmaStarCoarse U (adjointCoeffField a) sigmaStar)
(hKAdj : IsKappaCoarse U (adjointCoeffField a) sigmaStar (-kappa))
(hSigmaAdj : IsSigmaCoarse U (adjointCoeffField a) sigma sigmaStar (-kappa))
(hdet : IsUnit (Matrix.det sigmaStar))
(hInt : ResponseLinearIntegrabilityData U a)
(hIntAdj : ResponseLinearIntegrabilityData U (adjointCoeffField a))
(uFlux : (i : Fin d) → ScalarCanonicalMaximizer U (Pi.single i 1) 0 a)
(vFlux : (i : Fin d) → ScalarCanonicalMaximizer U (Pi.single i 1) 0 (adjointCoeffField a))
:
(fun (i : Fin d) =>
integralAverage U fun (x : Vec d) =>
(blockResponsePairHalfState a u.toAHarmonicFunctionMeanZero.toAHarmonicFunction
v.toAHarmonicFunctionMeanZero.toAHarmonicFunction).flux
x i) = q
The half-pair witness built from a primal maximizer at (0,q) and an
adjoint maximizer at (0,-q) has average flux equal to q.
theorem
HCPolySupport.blockResponse_pair_half_averageFlux_eq_of_scalarCanonicalMaximizers_zero_right_of_basisData
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
{sigma sigmaStar kappa : Mat d}
{q : Vec d}
(u : ScalarCanonicalMaximizer U 0 q a)
(v : ScalarCanonicalMaximizer U 0 (-q) (adjointCoeffField a))
(hS : IsSigmaStarCoarse U a sigmaStar)
(hK : IsKappaCoarse U a sigmaStar kappa)
(hSigma : IsSigmaCoarse U a sigma sigmaStar kappa)
(hSAdj : IsSigmaStarCoarse U (adjointCoeffField a) sigmaStar)
(hKAdj : IsKappaCoarse U (adjointCoeffField a) sigmaStar (-kappa))
(hSigmaAdj : IsSigmaCoarse U (adjointCoeffField a) sigma sigmaStar (-kappa))
(hdet : IsUnit (Matrix.det sigmaStar))
(hInt : ResponseLinearIntegrabilityData U a)
(hIntAdj : ResponseLinearIntegrabilityData U (adjointCoeffField a))
(basisFlux : ScalarCanonicalMaximizer.FluxBasisData U a)
(basisFluxAdj : ScalarCanonicalMaximizer.FluxBasisData U (adjointCoeffField a))
:
(fun (i : Fin d) =>
integralAverage U fun (x : Vec d) =>
(blockResponsePairHalfState a u.toAHarmonicFunctionMeanZero.toAHarmonicFunction
v.toAHarmonicFunctionMeanZero.toAHarmonicFunction).flux
x i) = q
Bundled basis-data wrapper for the previous average-flux identity.
theorem
HCPolySupport.blockResponse_pair_half_averagePotential_eq_zero_of_convexDomain
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
{lam Lam : ℝ}
{sigmaStar kappa : Mat d}
{q : Vec d}
(hConv : IsOpenBoundedConvexDomain U)
(hEll : IsEllipticFieldOn lam Lam U a)
(hvol : (MeasureTheory.volume U).toReal ≠ 0)
(u : ScalarCanonicalMaximizer U 0 q a)
(v : ScalarCanonicalMaximizer U 0 (-q) (adjointCoeffField a))
(hS : IsSigmaStarCoarse U a sigmaStar)
(hK : IsKappaCoarse U a sigmaStar kappa)
(hSAdj : IsSigmaStarCoarse U (adjointCoeffField a) sigmaStar)
(hKAdj : IsKappaCoarse U (adjointCoeffField a) sigmaStar (-kappa))
(hdet : IsUnit (Matrix.det sigmaStar))
:
(fun (i : Fin d) =>
integralAverage U fun (x : Vec d) =>
(blockResponsePairHalfState a u.toAHarmonicFunctionMeanZero.toAHarmonicFunction
v.toAHarmonicFunctionMeanZero.toAHarmonicFunction).potential
x i) = 0
Convex-domain wrapper for the zero-average-potential identity. The gradient basis-data packages are produced automatically from the Stage-6 canonical maximizer existence theorem.
theorem
HCPolySupport.exists_canonicalMaximizers_responsePair_half_averagePotential_eq_zero_right
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
{lam Lam : ℝ}
{sigmaStar kappa : Mat d}
{q : Vec d}
(hConv : IsOpenBoundedConvexDomain U)
(hEll : IsEllipticFieldOn lam Lam U a)
(hvol : (MeasureTheory.volume U).toReal ≠ 0)
(hS : IsSigmaStarCoarse U a sigmaStar)
(hK : IsKappaCoarse U a sigmaStar kappa)
(hSAdj : IsSigmaStarCoarse U (adjointCoeffField a) sigmaStar)
(hKAdj : IsKappaCoarse U (adjointCoeffField a) sigmaStar (-kappa))
(hdet : IsUnit (Matrix.det sigmaStar))
:
∃ (u : ScalarCanonicalMaximizer U 0 q a) (v : ScalarCanonicalMaximizer U 0 (-q) (adjointCoeffField a)),
(fun (i : Fin d) =>
integralAverage U fun (x : Vec d) =>
(blockResponsePairHalfState a u.toAHarmonicFunctionMeanZero.toAHarmonicFunction
v.toAHarmonicFunctionMeanZero.toAHarmonicFunction).potential
x i) = 0
Explicitly named existential convex-domain version of the previous average-potential identity. The scalar canonical maximizers are chosen internally from the bounded-open-convex existence theorem.
theorem
HCPolySupport.blockResponse_pair_half_averageFlux_eq_of_convexDomain
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
{lam Lam : ℝ}
{sigma sigmaStar kappa : Mat d}
{q : Vec d}
(hConv : IsOpenBoundedConvexDomain U)
(hEll : IsEllipticFieldOn lam Lam U a)
(hvol : (MeasureTheory.volume U).toReal ≠ 0)
(u : ScalarCanonicalMaximizer U 0 q a)
(v : ScalarCanonicalMaximizer U 0 (-q) (adjointCoeffField a))
(hS : IsSigmaStarCoarse U a sigmaStar)
(hK : IsKappaCoarse U a sigmaStar kappa)
(hSigma : IsSigmaCoarse U a sigma sigmaStar kappa)
(hSAdj : IsSigmaStarCoarse U (adjointCoeffField a) sigmaStar)
(hKAdj : IsKappaCoarse U (adjointCoeffField a) sigmaStar (-kappa))
(hSigmaAdj : IsSigmaCoarse U (adjointCoeffField a) sigma sigmaStar (-kappa))
(hdet : IsUnit (Matrix.det sigmaStar))
:
(fun (i : Fin d) =>
integralAverage U fun (x : Vec d) =>
(blockResponsePairHalfState a u.toAHarmonicFunctionMeanZero.toAHarmonicFunction
v.toAHarmonicFunctionMeanZero.toAHarmonicFunction).flux
x i) = q
Convex-domain wrapper for the average-flux identity. The flux basis-data packages are produced automatically from the Stage-6 canonical maximizer existence theorem.
theorem
HCPolySupport.exists_scalarCanonicalMaximizers_responsePair_half_averageFlux_eq_zero_right
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
{lam Lam : ℝ}
{sigma sigmaStar kappa : Mat d}
{q : Vec d}
(hConv : IsOpenBoundedConvexDomain U)
(hEll : IsEllipticFieldOn lam Lam U a)
(hvol : (MeasureTheory.volume U).toReal ≠ 0)
(hS : IsSigmaStarCoarse U a sigmaStar)
(hK : IsKappaCoarse U a sigmaStar kappa)
(hSigma : IsSigmaCoarse U a sigma sigmaStar kappa)
(hSAdj : IsSigmaStarCoarse U (adjointCoeffField a) sigmaStar)
(hKAdj : IsKappaCoarse U (adjointCoeffField a) sigmaStar (-kappa))
(hSigmaAdj : IsSigmaCoarse U (adjointCoeffField a) sigma sigmaStar (-kappa))
(hdet : IsUnit (Matrix.det sigmaStar))
:
∃ (u : ScalarCanonicalMaximizer U 0 q a) (v : ScalarCanonicalMaximizer U 0 (-q) (adjointCoeffField a)),
(fun (i : Fin d) =>
integralAverage U fun (x : Vec d) =>
(blockResponsePairHalfState a u.toAHarmonicFunctionMeanZero.toAHarmonicFunction
v.toAHarmonicFunctionMeanZero.toAHarmonicFunction).flux
x i) = q
Explicitly named existential convex-domain version of the previous average-flux identity. The scalar canonical maximizers are chosen internally from bounded-open-convex existence.
theorem
HCPolySupport.blockResponseIntegrand_integrableOn_pair_half_of_isEllipticFieldOn
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
{lam Lam : ℝ}
(hEll : IsEllipticFieldOn lam Lam U a)
(P Q : BlockVec d)
(u : AHarmonicFunction a U)
(v : AHarmonicFunction (adjointCoeffField a) U)
: