High-contrast homogenization: Provider.Response.PreYoungAdjointProjectionGeometry

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

Finite projection geometry for adjoint optimizer readouts

The adjoint optimizer is the canonical optimizer for the transposed coefficient sample. Consequently both adjoint block components inherit the primal finite-projection geometry, with separate scalar loads for the gradient and flux readouts.

theorem HCPolySupport.HighContrast.Response.integrableOn_diagonalWeakAdjointState_fst_component_of_aligned {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) {k t : ℤ} (hkt : k ≤ t) {w : Fin d → ℤ} (hw : w ∈ alignedIndex q k t) (a : CoeffSpace d) (p r : Vec d) (i : Fin d) : MeasureTheory.IntegrableOn (fun (x : Vec d) => (diagonalWeakAdjointState hq t a p r x).1 i) (adaptedCellAt q k w) MeasureTheory.volume

A gradient component of the adjoint terminal optimizer is integrable on every aligned subcell.

theorem HCPolySupport.HighContrast.Response.integrableOn_diagonalWeakAdjointState_snd_component_of_aligned {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) {k t : ℤ} (hkt : k ≤ t) {w : Fin d → ℤ} (hw : w ∈ alignedIndex q k t) (a : CoeffSpace d) (p r : Vec d) (i : Fin d) : MeasureTheory.IntegrableOn (fun (x : Vec d) => (diagonalWeakAdjointState hq t a p r x).2 i) (adaptedCellAt q k w) MeasureTheory.volume

A flux component of the adjoint terminal optimizer is integrable on every aligned subcell.

theorem HCPolySupport.HighContrast.Response.integrableOn_vecDot_diagonalWeakAdjointState_pullback {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) {s t : ℤ} (hst : s ≤ t) {z : Fin d → ℤ} (hz : z ∈ alignedIndex q s t) (a : CoeffSpace d) (p r Qcen : Vec d) : MeasureTheory.IntegrableOn (fun (y : Vec d) => vecDot Qcen (diagonalWeakAdjointState hq t a p r (matVecMul q y)).1) (cubeSet (translateCube z (originCube d s))) MeasureTheory.volume

The scalar adjoint gradient readout is integrable on a pulled-back parent cube.

theorem HCPolySupport.HighContrast.Response.integrableOn_vecDot_diagonalWeakAdjointState_flux_pullback {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) {s t : ℤ} (hst : s ≤ t) {z : Fin d → ℤ} (hz : z ∈ alignedIndex q s t) (a : CoeffSpace d) (p r Pcen : Vec d) : MeasureTheory.IntegrableOn (fun (y : Vec d) => vecDot Pcen (diagonalWeakAdjointState hq t a p r (matVecMul q y)).2) (cubeSet (translateCube z (originCube d s))) MeasureTheory.volume

The scalar adjoint flux readout is integrable on a pulled-back parent cube.

theorem HCPolySupport.HighContrast.Response.abs_cutoff_projected_adjoint_gradient_pairing_subSkew_le_nested_depth_sum {d : ℕ} [NeZero d] {q : Mat d} (hq : Matrix.PosDef q) {s t : ℤ} (hst : s ≤ t) {z : Fin d → ℤ} (hz : z ∈ alignedIndex q s t) (g : Mat d) (hg : IsSkewMat g) (a : CoeffSpace d) (p r Qcen : Vec d) (N : ℕ) : have R := translateCube z (originCube d s); have phi := fun (y : Vec d) => adaptedPreYoungCutoff q hq t (matVecMul q y); have f := fun (y : Vec d) => phi y - cubeAverage R phi; have F := diagonalWeakAdjointState hq t (a.subSkew g hg) p r; have G := fun (y : Vec d) => vecDot Qcen (F (matVecMul q y)).1; |cubeBesovPairing R f (cubeProjection R N G)| ≤ ∑ j ∈ Finset.range N, 32 * ↑d ^ 2 * smoothTransitionProfile.derivBound * 3 ^ (-(t - s + ↑j)) * avsum (alignedIndex q (s - ↑(j + 1)) s) fun (w : Fin d → ℤ) => |vecDot Qcen (blockCellAverage (adaptedCellAt q (s - ↑(j + 1)) (nestedLabel (s - ↑(j + 1)) s z w)) F).1|

The finite projected adjoint gradient pairing has the nested depth-sum bound.

theorem HCPolySupport.HighContrast.Response.abs_cutoff_projected_adjoint_flux_pairing_subSkew_le_nested_depth_sum {d : ℕ} [NeZero d] {q : Mat d} (hq : Matrix.PosDef q) {s t : ℤ} (hst : s ≤ t) {z : Fin d → ℤ} (hz : z ∈ alignedIndex q s t) (g : Mat d) (hg : IsSkewMat g) (a : CoeffSpace d) (p r Pcen : Vec d) (N : ℕ) : have R := translateCube z (originCube d s); have phi := fun (y : Vec d) => adaptedPreYoungCutoff q hq t (matVecMul q y); have f := fun (y : Vec d) => phi y - cubeAverage R phi; have F := diagonalWeakAdjointState hq t (a.subSkew g hg) p r; have G := fun (y : Vec d) => vecDot Pcen (F (matVecMul q y)).2; |cubeBesovPairing R f (cubeProjection R N G)| ≤ ∑ j ∈ Finset.range N, 32 * ↑d ^ 2 * smoothTransitionProfile.derivBound * 3 ^ (-(t - s + ↑j)) * avsum (alignedIndex q (s - ↑(j + 1)) s) fun (w : Fin d → ℤ) => |vecDot Pcen (blockCellAverage (adaptedCellAt q (s - ↑(j + 1)) (nestedLabel (s - ↑(j + 1)) s z w)) F).2|

The finite projected adjoint flux pairing has the nested depth-sum bound.

noncomputable def HCPolySupport.HighContrast.Response.adjointGradientProjectedOscillation {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (s t : ℤ) (g : Mat d) (hg : IsSkewMat g) (p r Qcen : Vec d) (N : ℕ) (a : CoeffSpace d) : ℝ

The finite-depth adjoint gradient oscillation.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.HighContrast.Response.adjointGradientPhysicalOscillation {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (s t : ℤ) (g : Mat d) (hg : IsSkewMat g) (p r Qcen : Vec d) (a : CoeffSpace d) : ℝ

The full physical adjoint gradient oscillation.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.HighContrast.Response.adjointFluxProjectedOscillation {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (s t : ℤ) (g : Mat d) (hg : IsSkewMat g) (p r Pcen : Vec d) (N : ℕ) (a : CoeffSpace d) : ℝ

The finite-depth adjoint flux oscillation.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.HighContrast.Response.adjointFluxPhysicalOscillation {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (s t : ℤ) (g : Mat d) (hg : IsSkewMat g) (p r Pcen : Vec d) (a : CoeffSpace d) : ℝ

The full physical adjoint flux oscillation.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.HighContrast.Response.abs_adjoint_gradient_projected_oscillation_le_nested_depth_sum {d : ℕ} [NeZero d] {q : Mat d} (hq : Matrix.PosDef q) {s t : ℤ} (hst : s ≤ t) (g : Mat d) (hg : IsSkewMat g) (p r Qcen : Vec d) (N : ℕ) (a : CoeffSpace d) : |adjointGradientProjectedOscillation hq s t g hg p r Qcen N a| ≤ ∑ j ∈ Finset.range N, 32 * ↑d ^ 2 * smoothTransitionProfile.derivBound * 3 ^ (-(t - s + ↑j)) * avsum (alignedIndex q s t) fun (z : Fin d → ℤ) => avsum (alignedIndex q (s - ↑(j + 1)) s) fun (w : Fin d → ℤ) => |vecDot Qcen (blockCellAverage (adaptedCellAt q (s - ↑(j + 1)) (nestedLabel (s - ↑(j + 1)) s z w)) (diagonalWeakAdjointState hq t (a.subSkew g hg) p r)).1|

The projected adjoint gradient oscillation obeys the nested depth-sum estimate.

theorem HCPolySupport.HighContrast.Response.abs_adjoint_flux_projected_oscillation_le_nested_depth_sum {d : ℕ} [NeZero d] {q : Mat d} (hq : Matrix.PosDef q) {s t : ℤ} (hst : s ≤ t) (g : Mat d) (hg : IsSkewMat g) (p r Pcen : Vec d) (N : ℕ) (a : CoeffSpace d) : |adjointFluxProjectedOscillation hq s t g hg p r Pcen N a| ≤ ∑ j ∈ Finset.range N, 32 * ↑d ^ 2 * smoothTransitionProfile.derivBound * 3 ^ (-(t - s + ↑j)) * avsum (alignedIndex q s t) fun (z : Fin d → ℤ) => avsum (alignedIndex q (s - ↑(j + 1)) s) fun (w : Fin d → ℤ) => |vecDot Pcen (blockCellAverage (adaptedCellAt q (s - ↑(j + 1)) (nestedLabel (s - ↑(j + 1)) s z w)) (diagonalWeakAdjointState hq t (a.subSkew g hg) p r)).2|

The projected adjoint flux oscillation obeys the nested depth-sum estimate.

theorem HCPolySupport.HighContrast.Response.adjoint_gradient_cutoff_oscillation_eq_unprojected_pairing {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (s t : ℤ) (w : Fin d → ℤ) (F : Vec d → BlockVec d) (Qcen : Vec d) : have R := translateCube w (originCube d s); have phi := fun (y : Vec d) => adaptedPreYoungCutoff q hq t (matVecMul q y); have f := fun (y : Vec d) => phi y - cubeAverage R phi; have G := fun (y : Vec d) => vecDot Qcen (F (matVecMul q y)).1; (volumeAverage (adaptedCellAt q s w) fun (x : Vec d) => (adaptedPreYoungCutoff q hq t x - volumeAverage (adaptedCellAt q s w) (adaptedPreYoungCutoff q hq t)) * vecDot Qcen (F x).1) = cubeBesovPairing R f G

The physical adjoint gradient oscillation is the unprojected scalar pairing on the reference cube.

theorem HCPolySupport.HighContrast.Response.adjoint_flux_cutoff_oscillation_eq_unprojected_pairing {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (s t : ℤ) (w : Fin d → ℤ) (F : Vec d → BlockVec d) (Pcen : Vec d) : have R := translateCube w (originCube d s); have phi := fun (y : Vec d) => adaptedPreYoungCutoff q hq t (matVecMul q y); have f := fun (y : Vec d) => phi y - cubeAverage R phi; have G := fun (y : Vec d) => vecDot Pcen (F (matVecMul q y)).2; (volumeAverage (adaptedCellAt q s w) fun (x : Vec d) => (adaptedPreYoungCutoff q hq t x - volumeAverage (adaptedCellAt q s w) (adaptedPreYoungCutoff q hq t)) * vecDot Pcen (F x).2) = cubeBesovPairing R f G

The physical adjoint flux oscillation is the unprojected scalar pairing on the reference cube.