High-contrast homogenization: Provider.Response.PreYoungRemainingPhysicalRows #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Literal physical cutoff rows #
The three remaining physical projection limits are rewritten as the literal cutoff-oscillation rows in the primal and adjoint mean decompositions.
Primal flux row #
theorem
HCPolySupport.HighContrast.Response.integral_primal_flux_physical_oscillation_eq_cutoff_row
{d : ℕ}
[NeZero d]
{P : MeasureTheory.Measure (CoeffSpace d)}
[MeasureTheory.IsProbabilityMeasure P]
{q m0 : Mat d}
(hq : Matrix.PosDef q)
(hm0 : Matrix.PosDef m0)
{s t : ℤ}
(hst : s ≤ t)
(g : Mat d)
(hg : IsSkewMat g)
(p r Pcen : Vec d)
(hweak : profilePrimalWeakQuantity P m0 hq t (fun (a : CoeffSpace d) => a.subSkew g hg) p r ≠ ⊤)
:
∫ (a : CoeffSpace d), primalFluxPhysicalOscillation hq s t g hg p r Pcen a ∂P = avsum (alignedIndex q s t) fun (z : Fin d → ℤ) =>
∑ i : Fin d,
Pcen i * ∫ (a : CoeffSpace d), volumeAverage (adaptedCellAt q s z) fun (x : Vec d) =>
(adaptedPreYoungCutoff q hq t x - volumeAverage (adaptedCellAt q s z) (adaptedPreYoungCutoff q hq t)) * toFullBlockVec (diagonalWeakState hq t (a.subSkew g hg) p r x) (Sum.inr i) ∂P
Annealed integration of the physical primal flux pairing equals the coordinate cutoff-oscillation row.
Adjoint gradient row #
theorem
HCPolySupport.HighContrast.Response.integral_adjoint_gradient_physical_oscillation_eq_cutoff_row
{d : ℕ}
[NeZero d]
{P : MeasureTheory.Measure (CoeffSpace d)}
[MeasureTheory.IsProbabilityMeasure P]
{q m0 : Mat d}
(hq : Matrix.PosDef q)
(hm0 : Matrix.PosDef m0)
{s t : ℤ}
(hst : s ≤ t)
(g : Mat d)
(hg : IsSkewMat g)
(p r Qcen : Vec d)
(hweak : profileAdjointWeakQuantity P m0 hq t (fun (a : CoeffSpace d) => a.subSkew g hg) p r ≠ ⊤)
:
∫ (a : CoeffSpace d), adjointGradientPhysicalOscillation hq s t g hg p r Qcen a ∂P = avsum (alignedIndex q s t) fun (z : Fin d → ℤ) =>
∑ i : Fin d,
Qcen i * ∫ (a : CoeffSpace d), volumeAverage (adaptedCellAt q s z) fun (x : Vec d) =>
(adaptedPreYoungCutoff q hq t x - volumeAverage (adaptedCellAt q s z) (adaptedPreYoungCutoff q hq t)) * toFullBlockVec (diagonalWeakAdjointState hq t (a.subSkew g hg) p r x) (Sum.inl i) ∂P
Annealed integration of the physical adjoint gradient pairing equals the coordinate cutoff-oscillation row.
Adjoint flux row #
theorem
HCPolySupport.HighContrast.Response.integral_adjoint_flux_physical_oscillation_eq_cutoff_row
{d : ℕ}
[NeZero d]
{P : MeasureTheory.Measure (CoeffSpace d)}
[MeasureTheory.IsProbabilityMeasure P]
{q m0 : Mat d}
(hq : Matrix.PosDef q)
(hm0 : Matrix.PosDef m0)
{s t : ℤ}
(hst : s ≤ t)
(g : Mat d)
(hg : IsSkewMat g)
(p r Pcen : Vec d)
(hweak : profileAdjointWeakQuantity P m0 hq t (fun (a : CoeffSpace d) => a.subSkew g hg) p r ≠ ⊤)
:
∫ (a : CoeffSpace d), adjointFluxPhysicalOscillation hq s t g hg p r Pcen a ∂P = avsum (alignedIndex q s t) fun (z : Fin d → ℤ) =>
∑ i : Fin d,
Pcen i * ∫ (a : CoeffSpace d), volumeAverage (adaptedCellAt q s z) fun (x : Vec d) =>
(adaptedPreYoungCutoff q hq t x - volumeAverage (adaptedCellAt q s z) (adaptedPreYoungCutoff q hq t)) * toFullBlockVec (diagonalWeakAdjointState hq t (a.subSkew g hg) p r x) (Sum.inr i) ∂P
Annealed integration of the physical adjoint flux pairing equals the coordinate cutoff-oscillation row.