High-contrast homogenization: Provider.Response.AdaptedFiveTermSplit

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

Cutoff-mean splitting on adapted cells

An aligned cutoff-defect mean splits into parent--child defect and within-cell oscillation; stationarity cancels the remaining child-optimizer mean.

theorem HCPolySupport.HighContrast.Response.vecDot_profilePrimalCutoffMean_fst_eq_defect_add_oscillation {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] (hstat : IsStationaryLaw P) {l s t : ℤ} {q : Mat d} (hgrid : IsRoundedGrid l q) (hls : l ≤ s) (hst : s ≤ t) (hint : HasFiniteAdaptedMean P q s) (g : Mat d) (hg : IsSkewMat g) (p r Qcen : Vec d) : have hq := ⋯; have X := fun (a : CoeffSpace d) => diagonalWeakState hq t (a.subSkew g hg) p r; have Y := fun (w : Fin d → ℤ) (a : CoeffSpace d) => diagonalWeakChildState hq s w (a.subSkew g hg) p r; ((∀ w ∈ alignedIndex q s t, ∀ (alpha : BlockCoord d), MeasureTheory.Integrable (fun (a : CoeffSpace d) => toFullBlockVec (blockCellAverage (adaptedCellAt q s w) (X a)) alpha) P) ∧ ∀ w ∈ alignedIndex q s t, ∀ (alpha : BlockCoord d), MeasureTheory.Integrable (fun (a : CoeffSpace d) => volumeAverage (adaptedCellAt q s w) fun (x : Vec d) => (adaptedPreYoungCutoff q hq t x - volumeAverage (adaptedCellAt q s w) (adaptedPreYoungCutoff q hq t)) * toFullBlockVec (X a x) alpha) P) → vecDot Qcen (profilePrimalCutoffMean P hq t (fun (a : CoeffSpace d) => a.subSkew g hg) (adaptedPreYoungCutoff q hq t) p r).1 = (avsum (alignedIndex q s t) fun (w : Fin d → ℤ) => (1 - volumeAverage (adaptedCellAt q s w) (adaptedPreYoungCutoff q hq t)) * ∑ i : Fin d, Qcen i * (∫ (a : CoeffSpace d), toFullBlockVec (blockCellAverage (adaptedCellAt q s w) (Y w a)) (Sum.inl i) ∂P - ∫ (a : CoeffSpace d), toFullBlockVec (blockCellAverage (adaptedCellAt q s w) (X a)) (Sum.inl i) ∂P)) + avsum (alignedIndex q s t) fun (w : Fin d → ℤ) => ∑ i : Fin d, Qcen i * ∫ (a : CoeffSpace d), volumeAverage (adaptedCellAt q s w) fun (x : Vec d) => (adaptedPreYoungCutoff q hq t x - volumeAverage (adaptedCellAt q s w) (adaptedPreYoungCutoff q hq t)) * toFullBlockVec (X a x) (Sum.inl i) ∂P

The primal gradient cutoff mean splits into its defect and oscillation halves.

theorem HCPolySupport.HighContrast.Response.vecDot_profilePrimalCutoffMean_snd_eq_defect_add_oscillation {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] (hstat : IsStationaryLaw P) {l s t : ℤ} {q : Mat d} (hgrid : IsRoundedGrid l q) (hls : l ≤ s) (hst : s ≤ t) (hint : HasFiniteAdaptedMean P q s) (g : Mat d) (hg : IsSkewMat g) (p r Pcen : Vec d) : have hq := ⋯; have X := fun (a : CoeffSpace d) => diagonalWeakState hq t (a.subSkew g hg) p r; have Y := fun (w : Fin d → ℤ) (a : CoeffSpace d) => diagonalWeakChildState hq s w (a.subSkew g hg) p r; ((∀ w ∈ alignedIndex q s t, ∀ (alpha : BlockCoord d), MeasureTheory.Integrable (fun (a : CoeffSpace d) => toFullBlockVec (blockCellAverage (adaptedCellAt q s w) (X a)) alpha) P) ∧ ∀ w ∈ alignedIndex q s t, ∀ (alpha : BlockCoord d), MeasureTheory.Integrable (fun (a : CoeffSpace d) => volumeAverage (adaptedCellAt q s w) fun (x : Vec d) => (adaptedPreYoungCutoff q hq t x - volumeAverage (adaptedCellAt q s w) (adaptedPreYoungCutoff q hq t)) * toFullBlockVec (X a x) alpha) P) → vecDot Pcen (profilePrimalCutoffMean P hq t (fun (a : CoeffSpace d) => a.subSkew g hg) (adaptedPreYoungCutoff q hq t) p r).2 = (avsum (alignedIndex q s t) fun (w : Fin d → ℤ) => (1 - volumeAverage (adaptedCellAt q s w) (adaptedPreYoungCutoff q hq t)) * ∑ i : Fin d, Pcen i * (∫ (a : CoeffSpace d), toFullBlockVec (blockCellAverage (adaptedCellAt q s w) (Y w a)) (Sum.inr i) ∂P - ∫ (a : CoeffSpace d), toFullBlockVec (blockCellAverage (adaptedCellAt q s w) (X a)) (Sum.inr i) ∂P)) + avsum (alignedIndex q s t) fun (w : Fin d → ℤ) => ∑ i : Fin d, Pcen i * ∫ (a : CoeffSpace d), volumeAverage (adaptedCellAt q s w) fun (x : Vec d) => (adaptedPreYoungCutoff q hq t x - volumeAverage (adaptedCellAt q s w) (adaptedPreYoungCutoff q hq t)) * toFullBlockVec (X a x) (Sum.inr i) ∂P

The primal flux cutoff mean splits into its defect and oscillation halves.

theorem HCPolySupport.HighContrast.Response.vecDot_profileAdjointCutoffMean_fst_eq_defect_add_oscillation {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] (hstat : IsStationaryLaw P) {l s t : ℤ} {q : Mat d} (hgrid : IsRoundedGrid l q) (hls : l ≤ s) (hst : s ≤ t) (hint : HasFiniteAdaptedMean P q s) (g : Mat d) (hg : IsSkewMat g) (p r Qcen : Vec d) : have hq := ⋯; have X := fun (a : CoeffSpace d) => diagonalWeakState hq t (a.subSkew g hg).transpose p r; have Y := fun (w : Fin d → ℤ) (a : CoeffSpace d) => diagonalWeakChildState hq s w (a.subSkew g hg).transpose p r; ((∀ w ∈ alignedIndex q s t, ∀ (alpha : BlockCoord d), MeasureTheory.Integrable (fun (a : CoeffSpace d) => toFullBlockVec (blockCellAverage (adaptedCellAt q s w) (X a)) alpha) P) ∧ ∀ w ∈ alignedIndex q s t, ∀ (alpha : BlockCoord d), MeasureTheory.Integrable (fun (a : CoeffSpace d) => volumeAverage (adaptedCellAt q s w) fun (x : Vec d) => (adaptedPreYoungCutoff q hq t x - volumeAverage (adaptedCellAt q s w) (adaptedPreYoungCutoff q hq t)) * toFullBlockVec (X a x) alpha) P) → vecDot Qcen (profileAdjointCutoffMean P hq t (fun (a : CoeffSpace d) => a.subSkew g hg) (adaptedPreYoungCutoff q hq t) p r).1 = (avsum (alignedIndex q s t) fun (w : Fin d → ℤ) => (1 - volumeAverage (adaptedCellAt q s w) (adaptedPreYoungCutoff q hq t)) * ∑ i : Fin d, Qcen i * (∫ (a : CoeffSpace d), toFullBlockVec (blockCellAverage (adaptedCellAt q s w) (Y w a)) (Sum.inl i) ∂P - ∫ (a : CoeffSpace d), toFullBlockVec (blockCellAverage (adaptedCellAt q s w) (X a)) (Sum.inl i) ∂P)) + avsum (alignedIndex q s t) fun (w : Fin d → ℤ) => ∑ i : Fin d, Qcen i * ∫ (a : CoeffSpace d), volumeAverage (adaptedCellAt q s w) fun (x : Vec d) => (adaptedPreYoungCutoff q hq t x - volumeAverage (adaptedCellAt q s w) (adaptedPreYoungCutoff q hq t)) * toFullBlockVec (X a x) (Sum.inl i) ∂P

The adjoint gradient cutoff mean has the independently canceled split.

theorem HCPolySupport.HighContrast.Response.vecDot_profileAdjointCutoffMean_snd_eq_defect_add_oscillation {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] (hstat : IsStationaryLaw P) {l s t : ℤ} {q : Mat d} (hgrid : IsRoundedGrid l q) (hls : l ≤ s) (hst : s ≤ t) (hint : HasFiniteAdaptedMean P q s) (g : Mat d) (hg : IsSkewMat g) (p r Pcen : Vec d) : have hq := ⋯; have X := fun (a : CoeffSpace d) => diagonalWeakState hq t (a.subSkew g hg).transpose p r; have Y := fun (w : Fin d → ℤ) (a : CoeffSpace d) => diagonalWeakChildState hq s w (a.subSkew g hg).transpose p r; ((∀ w ∈ alignedIndex q s t, ∀ (alpha : BlockCoord d), MeasureTheory.Integrable (fun (a : CoeffSpace d) => toFullBlockVec (blockCellAverage (adaptedCellAt q s w) (X a)) alpha) P) ∧ ∀ w ∈ alignedIndex q s t, ∀ (alpha : BlockCoord d), MeasureTheory.Integrable (fun (a : CoeffSpace d) => volumeAverage (adaptedCellAt q s w) fun (x : Vec d) => (adaptedPreYoungCutoff q hq t x - volumeAverage (adaptedCellAt q s w) (adaptedPreYoungCutoff q hq t)) * toFullBlockVec (X a x) alpha) P) → vecDot Pcen (profileAdjointCutoffMean P hq t (fun (a : CoeffSpace d) => a.subSkew g hg) (adaptedPreYoungCutoff q hq t) p r).2 = (avsum (alignedIndex q s t) fun (w : Fin d → ℤ) => (1 - volumeAverage (adaptedCellAt q s w) (adaptedPreYoungCutoff q hq t)) * ∑ i : Fin d, Pcen i * (∫ (a : CoeffSpace d), toFullBlockVec (blockCellAverage (adaptedCellAt q s w) (Y w a)) (Sum.inr i) ∂P - ∫ (a : CoeffSpace d), toFullBlockVec (blockCellAverage (adaptedCellAt q s w) (X a)) (Sum.inr i) ∂P)) + avsum (alignedIndex q s t) fun (w : Fin d → ℤ) => ∑ i : Fin d, Pcen i * ∫ (a : CoeffSpace d), volumeAverage (adaptedCellAt q s w) fun (x : Vec d) => (adaptedPreYoungCutoff q hq t x - volumeAverage (adaptedCellAt q s w) (adaptedPreYoungCutoff q hq t)) * toFullBlockVec (X a x) (Sum.inr i) ∂P

The adjoint flux cutoff mean has the independently canceled split.