High-contrast homogenization: Provider.Response.PreYoungFixedGridPhysicalRows

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

Physical cutoff-oscillation rows, fixed grid

Fixed-rounded-grid sibling of HCPoly.Provider.Response.PreYoungPrimalPhysicalRow, HCPoly.Provider.Response.PreYoungRemainingPhysicalRows: 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.of_real_abs_primal_cutoff_oscillation_row_le {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 : profilePrimalWeakQuantity P m0 ⋯ t (fun (a : CoeffSpace d) => a.subSkew g hg) p r ≠ ⊤) : ENNReal.ofReal |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 ⋯ t x - volumeAverage (adaptedCellAt q s z) (adaptedPreYoungCutoff q ⋯ t)) * toFullBlockVec (diagonalWeakState ⋯ t (a.subSkew g hg) p r x) (Sum.inl i) ∂P| ≤ ENNReal.ofReal (preYoungRowCoefficient d * 3 ^ (-(↑t - ↑s)) * √(∫ (a : CoeffSpace d), Book.Ch02.responseJ (adaptedDomain ⋯ t) ((a.subSkew g hg).coeffOn (adaptedDomain ⋯ t)) p r ∂P)) * profilePrimalHattedEarlierRow P q g s Pcen Qcen ^ (1 / 2)

The literal primal gradient-slot cutoff oscillation is controlled by the all-earlier hatted row.

theorem HCPolySupport.HighContrast.Response.FixedGrid.of_real_abs_primal_flux_cutoff_oscillation_row_le {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 : profilePrimalWeakQuantity P m0 ⋯ t (fun (a : CoeffSpace d) => a.subSkew g hg) p r ≠ ⊤) : ENNReal.ofReal |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 ⋯ t x - volumeAverage (adaptedCellAt q s z) (adaptedPreYoungCutoff q ⋯ t)) * toFullBlockVec (diagonalWeakState ⋯ t (a.subSkew g hg) p r x) (Sum.inr i) ∂P| ≤ ENNReal.ofReal (preYoungRowCoefficient d * 3 ^ (-(↑t - ↑s)) * √(∫ (a : CoeffSpace d), Book.Ch02.responseJ (adaptedDomain ⋯ t) ((a.subSkew g hg).coeffOn (adaptedDomain ⋯ t)) p r ∂P)) * profilePrimalHattedEarlierRow P q g s Pcen Qcen ^ (1 / 2)

The literal primal flux cutoff oscillation is controlled by the all-earlier primal row.

theorem HCPolySupport.HighContrast.Response.FixedGrid.of_real_abs_adjoint_gradient_cutoff_oscillation_row_le {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 ≠ ⊤) : ENNReal.ofReal |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 ⋯ t x - volumeAverage (adaptedCellAt q s z) (adaptedPreYoungCutoff q ⋯ t)) * toFullBlockVec (diagonalWeakAdjointState ⋯ t (a.subSkew g hg) p r x) (Sum.inl i) ∂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 literal adjoint gradient cutoff oscillation is controlled by the all-earlier adjoint row.

theorem HCPolySupport.HighContrast.Response.FixedGrid.of_real_abs_adjoint_flux_cutoff_oscillation_row_le {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 ≠ ⊤) : ENNReal.ofReal |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 ⋯ t x - volumeAverage (adaptedCellAt q s z) (adaptedPreYoungCutoff q ⋯ t)) * toFullBlockVec (diagonalWeakAdjointState ⋯ t (a.subSkew g hg) p r x) (Sum.inr i) ∂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 literal adjoint flux cutoff oscillation is controlled by the all-earlier adjoint row.