High-contrast homogenization: Provider.Response.PreYoungPrimalFluxProjectionGeometry

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

Finite projection geometry for the primal flux readout

The second block component of the primal optimizer is handled by the same finite cube projections as the first component. Swapping the two components of an arbitrary doubled field makes the common projection geometry directly reusable while preserving the physical flux pairing.

theorem HCPolySupport.HighContrast.Response.integrableOn_diagonalWeakState_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) => (diagonalWeakState hq t a p r x).2 i) (adaptedCellAt q k w) MeasureTheory.volume

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

theorem HCPolySupport.HighContrast.Response.integrableOn_vecDot_diagonalWeakState_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 (diagonalWeakState hq t a p r (matVecMul q y)).2) (cubeSet (translateCube z (originCube d s))) MeasureTheory.volume

The scalar flux readout remains integrable after pulling an aligned cell back to its reference cube.

theorem HCPolySupport.HighContrast.Response.abs_cutoff_projected_primal_flux_pairing_le_nested_depth_sum {d : ℕ} [NeZero d] {q : Mat d} (hq : Matrix.PosDef q) (s t : ℤ) (z : Fin d → ℤ) (F : Vec d → BlockVec d) (Pcen : Vec d) (N : ℕ) (hGInt : MeasureTheory.IntegrableOn (fun (y : Vec d) => vecDot Pcen (F (matVecMul q y)).2) (cubeSet (translateCube z (originCube d s))) MeasureTheory.volume) (hF : ∀ j < N, ∀ w ∈ alignedIndex q (s - ↑(j + 1)) s, ∀ (i : Fin d), MeasureTheory.IntegrableOn (fun (x : Vec d) => (F x).2 i) (adaptedCellAt q (s - ↑(j + 1)) (nestedLabel (s - ↑(j + 1)) s z w)) MeasureTheory.volume) : 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 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|

A projected scalar flux pairing is controlled by the nested-cell depth sum with the sharp cutoff coefficient.

theorem HCPolySupport.HighContrast.Response.abs_cutoff_projected_primal_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 := diagonalWeakState 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 preceding projected flux estimate specialized to a recentered primal optimizer sample.

noncomputable def HCPolySupport.HighContrast.Response.primalFluxProjectedOscillation {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 primal flux oscillation, averaged over terminal parents.

Equations

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

noncomputable def HCPolySupport.HighContrast.Response.primalFluxPhysicalOscillation {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 primal flux oscillation, averaged over terminal parents.

Equations

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

theorem HCPolySupport.HighContrast.Response.abs_primal_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) : |primalFluxProjectedOscillation 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)) (diagonalWeakState hq t (a.subSkew g hg) p r)).2|

The projected primal flux oscillation obeys the terminal-parent nested depth-sum estimate.

theorem HCPolySupport.HighContrast.Response.primal_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 primal flux cutoff oscillation is the unprojected Besov pairing on the reference cube.