High-contrast homogenization: Provider.Response.PreYoungFixedGridAdjointProjectedRows

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

Finite projected adjoint rows, fixed grid

Fixed-rounded-grid sibling of HCPoly.Provider.Response.PreYoungAdjointGradientProjectedRowBound, HCPoly.Provider.Response.PreYoungAdjointFluxProjectedRowBound: the grid stays rounded at the fixed alignment l while the generation window {s, t} moves, the aligned-cell integrability coming from the AlignedCellsIntegrable carrier instead of the window multiplier's carrier equality. The proof is unchanged apart from the window bundle replaced by the carrier.

theorem HCPolySupport.HighContrast.Response.FixedGrid.integrable_adjoint_gradient_projected_oscillation_and_integral_abs_le_scale_rows {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] (hstat : IsStationaryLaw P) {l : ℤ} {m0 q : Mat d} (hm0 : Matrix.PosDef m0) (hgrid : IsRoundedGrid l q) {s t : ℤ} (hls : l ≤ s) (hst : s ≤ t) (hcells : AlignedCellsIntegrable P q s t) (hblocks : ∀ (k : ℤ), l ≤ k → k ≤ t → HasFiniteAdaptedMean P q k ∧ Book.Ch02.BlockPosDef (adaptedMean P q k)) (g : Mat d) (hg : IsSkewMat g) (p r Pcen Qcen : Vec d) (hweak : profileAdjointWeakQuantity P m0 ⋯ t (fun (a : CoeffSpace d) => a.subSkew g hg) p r ≠ ⊤) (N : ℕ) : MeasureTheory.Integrable (adjointGradientProjectedOscillation ⋯ s t g hg p r Qcen N) P ∧ ∫ (a : CoeffSpace d), |adjointGradientProjectedOscillation ⋯ s t g hg p r Qcen N a| ∂P ≤ adaptedCutoffDerivativeCoeff d * 3 ^ (-(↑t - ↑s)) * ∑ k ∈ Finset.Icc (s - ↑N) s, 3 ^ (↑k - ↑s) * avsum (alignedIndex q k s) fun (w : Fin d → ℤ) => profileRowCellEnergy P ⋯ k s t w (fun (a : CoeffSpace d) => (a.subSkew g hg).transpose) p r * profileSchurLoadFlux (profileHattedAdjointBlock g (annealedBlock P (adaptedCellAt q k w))) Qcen

A finite projected adjoint gradient oscillation is integrable, and its expected absolute value is bounded by the corresponding finite weighted row.

theorem HCPolySupport.HighContrast.Response.FixedGrid.lintegral_adjoint_gradient_projected_oscillation_le_row {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] (hstat : IsStationaryLaw P) {l : ℤ} {m0 q : Mat d} (hm0 : Matrix.PosDef m0) (hgrid : IsRoundedGrid l q) {s t : ℤ} (hls : l ≤ s) (hst : s ≤ t) (hcells : AlignedCellsIntegrable P q s t) (hblocks : ∀ (k : ℤ), l ≤ k → k ≤ t → HasFiniteAdaptedMean P q k ∧ Book.Ch02.BlockPosDef (adaptedMean P q k)) (g : Mat d) (hg : IsSkewMat g) (p r Pcen Qcen : Vec d) (hweak : profileAdjointWeakQuantity P m0 ⋯ t (fun (a : CoeffSpace d) => a.subSkew g hg) p r ≠ ⊤) (N : ℕ) : ∫⁻ (a : CoeffSpace d), ENNReal.ofReal |adjointGradientProjectedOscillation ⋯ s t g hg p r Qcen N a| ∂P ≤ ENNReal.ofReal (preYoungRowCoefficient d * 3 ^ (-(↑t - ↑s)) * √(∫ (a : CoeffSpace d), Book.Ch02.responseJ (adaptedDomain ⋯ t) ((a.subSkew g hg).transpose.coeffOn (adaptedDomain ⋯ t)) p r ∂P)) * profileAdjointHattedEarlierRow P q g s Pcen Qcen ^ (1 / 2)

The absolute lower integral of every finite adjoint gradient projection has a common bound by the transposed all-earlier hatted row.

theorem HCPolySupport.HighContrast.Response.FixedGrid.integrable_adjoint_flux_projected_oscillation_and_integral_abs_le_scale_rows {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] (hstat : IsStationaryLaw P) {l : ℤ} {m0 q : Mat d} (hm0 : Matrix.PosDef m0) (hgrid : IsRoundedGrid l q) {s t : ℤ} (hls : l ≤ s) (hst : s ≤ t) (hcells : AlignedCellsIntegrable P q s t) (hblocks : ∀ (k : ℤ), l ≤ k → k ≤ t → HasFiniteAdaptedMean P q k ∧ Book.Ch02.BlockPosDef (adaptedMean P q k)) (g : Mat d) (hg : IsSkewMat g) (p r Pcen Qcen : Vec d) (hweak : profileAdjointWeakQuantity P m0 ⋯ t (fun (a : CoeffSpace d) => a.subSkew g hg) p r ≠ ⊤) (N : ℕ) : MeasureTheory.Integrable (adjointFluxProjectedOscillation ⋯ s t g hg p r Pcen N) P ∧ ∫ (a : CoeffSpace d), |adjointFluxProjectedOscillation ⋯ s t g hg p r Pcen N a| ∂P ≤ adaptedCutoffDerivativeCoeff d * 3 ^ (-(↑t - ↑s)) * ∑ k ∈ Finset.Icc (s - ↑N) s, 3 ^ (↑k - ↑s) * avsum (alignedIndex q k s) fun (w : Fin d → ℤ) => profileRowCellEnergy P ⋯ k s t w (fun (a : CoeffSpace d) => (a.subSkew g hg).transpose) p r * profileSchurLoadGradient (profileHattedAdjointBlock g (annealedBlock P (adaptedCellAt q k w))) Pcen

A finite projected adjoint flux oscillation is integrable, and its expected absolute value is bounded by the corresponding finite weighted row.

theorem HCPolySupport.HighContrast.Response.FixedGrid.lintegral_adjoint_flux_projected_oscillation_le_row {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] (hstat : IsStationaryLaw P) {l : ℤ} {m0 q : Mat d} (hm0 : Matrix.PosDef m0) (hgrid : IsRoundedGrid l q) {s t : ℤ} (hls : l ≤ s) (hst : s ≤ t) (hcells : AlignedCellsIntegrable P q s t) (hblocks : ∀ (k : ℤ), l ≤ k → k ≤ t → HasFiniteAdaptedMean P q k ∧ Book.Ch02.BlockPosDef (adaptedMean P q k)) (g : Mat d) (hg : IsSkewMat g) (p r Pcen Qcen : Vec d) (hweak : profileAdjointWeakQuantity P m0 ⋯ t (fun (a : CoeffSpace d) => a.subSkew g hg) p r ≠ ⊤) (N : ℕ) : ∫⁻ (a : CoeffSpace d), ENNReal.ofReal |adjointFluxProjectedOscillation ⋯ s t g hg p r Pcen N a| ∂P ≤ ENNReal.ofReal (preYoungRowCoefficient d * 3 ^ (-(↑t - ↑s)) * √(∫ (a : CoeffSpace d), Book.Ch02.responseJ (adaptedDomain ⋯ t) ((a.subSkew g hg).transpose.coeffOn (adaptedDomain ⋯ t)) p r ∂P)) * profileAdjointHattedEarlierRow P q g s Pcen Qcen ^ (1 / 2)

The absolute lower integral of every finite adjoint flux projection has a common bound by the transposed all-earlier hatted row.