High-contrast homogenization: Entry.Response.Rows.CellHalfCarrierBound #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The Cell Half of the Cutoff-Mean Row at the Response Carriers #
The cell half of the two cutoff-mean rows of p.response.transfer asserts that the modulus of the
dual pairing of the
cell part of the cutoff-mean defect against a state Y^∓ is at most √(L_s^∓) · √(2 tau^∓). This file assembles that bound from its established pieces: the abstract cell-pairing row
supplies the annealed Cauchy-Schwarz estimate and the stationarity collapse of the annealed head,
the per-cell dual pairing discharges its pathwise hypothesis at an almost-everywhere elliptic
response coefficient, the doubled deficit rescaling supplies the annealed flat deficit as 2 tau^∓, and the linearity of the crossed pairing together with mean cancellation rewrites the
abstract statement back into the pairing of the cell part against Y^∓. The result is the
carrier-level form of the cell half of the response-transfer estimate, for each sign.
The cell half of the cutoff-mean row on the carriers #
The cell half of the two cutoff-mean rows of p.response.transfer asserts that the modulus of the
dual pairing of the cell part of the cutoff-mean defect against Y^∓ is at most
√(L_s^∓) * √(2 tau^∓). This module assembles that statement from the established pieces: the
abstract cell-pairing row abs_integral_avsum_weighted_pairing_le_respLsMinus /
…Plus supplies the annealed Cauchy--Schwarz estimate and the collapse of the annealed head, the
per-cell pairing bound abs_dualPairing_diff_cellAverage_adaptedCellAtCenter_le discharges its
pathwise
hypothesis at the almost-everywhere elliptic response coefficient, the deficit rescaling
integral_avsum_two_subcellDeficit_eq_two_respTauMinus / …Plus discharges the value of the
annealed flat deficit, and the crossed-pairing linearity
vecDot_avsum_integral_eq_integral_avsum_pairing
together with the mean cancellation avsum_weighted_integral_cellAverage_subcellOptimizer_eq_zero
rewrites the abstract flat average back into the pairing of the cell part Ncell against Y^∓.
theorem
HCPolySupport.HighContrast.Multiscale.abs_vecDot_cellPart_respYMinus_le
{d : ℕ}
[NeZero d]
(P : MeasureTheory.Measure (CoeffSpace d))
[MeasureTheory.IsProbabilityMeasure P]
(hstat : IsStationaryLaw P)
(jStar : ℕ)
(hjStar : 2 * d ≤ 3 ^ jStar)
(F : BlockMat d)
(hm : Matrix.PosDef (explicitCanonicalMetric F))
(H : ℕ)
(s t : ℤ)
(ht : t = s + ↑H)
(hjs : ↑jStar ≤ s)
(e : Vec d)
(φ : Vec d → ℝ)
(hφ : IsResponseCutoff (respGrid jStar F) t φ)
(uM : (a : CoeffSpace d) → AHarmonicFunction (respCoeffMinus F a) (respCell jStar F t))
(hmax :
∀ (a : CoeffSpace d),
IsResponseMaximizer (respCell jStar F t) (respP (respMean P jStar F t) e) (respqMinus P jStar F t e)
(respCoeffMinus F a) (uM a))
(v :
(w : Fin d → ℤ) →
(a : CoeffSpace d) → AHarmonicFunction (respCoeffMinus F a) (adaptedCellAtCenter (respGrid jStar F) s w))
(hmaxV :
∀ w ∈ triadicIndexBox d H,
∀ (a : CoeffSpace d),
IsResponseMaximizer (adaptedCellAtCenter (respGrid jStar F) s w) (respP (respMean P jStar F t) e)
(respqMinus P jStar F t e) (respCoeffMinus F a) (v w a))
(hsum : Summable (respSourceLoadSummand P jStar F s (respCoeffMinus F) (respYMinus P jStar F t e)))
(hblk : ∀ (w : Fin d → ℤ), HasIntegrableCoarseBlock P (adaptedCellAtCenter (respGrid jStar F) s w))
(hrespint :
∀ (a : CoeffSpace d),
MeasureTheory.IntegrableOn
(scalarResponseIntegrand (respCell jStar F t) (respCoeffMinus F a) (respP (respMean P jStar F t) e)
(respqMinus P jStar F t e) (uM a))
(respCell jStar F t) MeasureTheory.volume)
(hJint :
∀ w ∈ triadicIndexBox d H,
MeasureTheory.Integrable
(fun (a : CoeffSpace d) =>
ResponseJ (adaptedCellAtCenter (respGrid jStar F) s w) (respP (respMean P jStar F t) e)
(respqMinus P jStar F t e) (respCoeffMinus F a))
P)
(hRint :
∀ w ∈ triadicIndexBox d H,
MeasureTheory.Integrable
(fun (a : CoeffSpace d) =>
volumeAverage (adaptedCellAtCenter (respGrid jStar F) s w)
(scalarResponseIntegrand (respCell jStar F t) (respCoeffMinus F a) (respP (respMean P jStar F t) e)
(respqMinus P jStar F t e) (uM a)))
P)
(hJt :
MeasureTheory.Integrable
(fun (a : CoeffSpace d) =>
respJ (respGrid jStar F) t (respP (respMean P jStar F t) e) (respqMinus P jStar F t e) (respCoeffMinus F a))
P)
(hJs :
MeasureTheory.Integrable
(fun (a : CoeffSpace d) =>
respJ (respGrid jStar F) s (respP (respMean P jStar F t) e) (respqMinus P jStar F t e) (respCoeffMinus F a))
P)
(hUL :
∀ w ∈ triadicIndexBox d H,
∀ (a : CoeffSpace d),
0 ≤ vecDot (respYMinus P jStar F t e).1
(matVecMul (coarseBlockMatrix (adaptedCellAtCenter (respGrid jStar F) s w) (respCoeffMinus F a)).upperLeft
(respYMinus P jStar F t e).1))
(hLR :
∀ w ∈ triadicIndexBox d H,
∀ (a : CoeffSpace d),
0 ≤ vecDot (respYMinus P jStar F t e).2
(matVecMul (coarseBlockMatrix (adaptedCellAtCenter (respGrid jStar F) s w) (respCoeffMinus F a)).lowerRight
(respYMinus P jStar F t e).2))
(hentUL :
∀ w ∈ triadicIndexBox d H,
∀ (i j : Fin d),
MeasureTheory.Integrable
(fun (a : CoeffSpace d) =>
(coarseBlockMatrix (adaptedCellAtCenter (respGrid jStar F) s w) (respCoeffMinus F a)).upperLeft i j)
P)
(hentLR :
∀ w ∈ triadicIndexBox d H,
∀ (i j : Fin d),
MeasureTheory.Integrable
(fun (a : CoeffSpace d) =>
(coarseBlockMatrix (adaptedCellAtCenter (respGrid jStar F) s w) (respCoeffMinus F a)).lowerRight i j)
P)
(hqUL :
∀ w ∈ triadicIndexBox d H,
MeasureTheory.Integrable
(fun (a : CoeffSpace d) =>
vecDot (respYMinus P jStar F t e).1
(matVecMul (coarseBlockMatrix (adaptedCellAtCenter (respGrid jStar F) s w) (respCoeffMinus F a)).upperLeft
(respYMinus P jStar F t e).1))
P)
(hqLR :
∀ w ∈ triadicIndexBox d H,
MeasureTheory.Integrable
(fun (a : CoeffSpace d) =>
vecDot (respYMinus P jStar F t e).2
(matVecMul (coarseBlockMatrix (adaptedCellAtCenter (respGrid jStar F) s w) (respCoeffMinus F a)).lowerRight
(respYMinus P jStar F t e).2))
P)
(hcross :
∀ w ∈ triadicIndexBox d H,
MeasureTheory.Integrable
(fun (a : CoeffSpace d) =>
√(vecDot (respYMinus P jStar F t e).1
(matVecMul (coarseBlockMatrix (adaptedCellAtCenter (respGrid jStar F) s w) (respCoeffMinus F a)).upperLeft
(respYMinus P jStar F t e).1)) * √(vecDot (respYMinus P jStar F t e).2
(matVecMul
(coarseBlockMatrix (adaptedCellAtCenter (respGrid jStar F) s w) (respCoeffMinus F a)).lowerRight
(respYMinus P jStar F t e).2)))
P)
(hsq :
∀ w ∈ triadicIndexBox d H,
MeasureTheory.Integrable
(fun (a : CoeffSpace d) =>
(√(vecDot (respYMinus P jStar F t e).1
(matVecMul
(coarseBlockMatrix (adaptedCellAtCenter (respGrid jStar F) s w) (respCoeffMinus F a)).upperLeft
(respYMinus P jStar F t e).1)) + √(vecDot (respYMinus P jStar F t e).2
(matVecMul
(coarseBlockMatrix (adaptedCellAtCenter (respGrid jStar F) s w) (respCoeffMinus F a)).lowerRight
(respYMinus P jStar F t e).2))) ^ 2)
P)
(hFint :
MeasureTheory.Integrable
(fun (a : CoeffSpace d) =>
(↑(triadicIndexBox d H).card)⁻¹ * ∑ w ∈ triadicIndexBox d H,
(√(vecDot (respYMinus P jStar F t e).1
(matVecMul
(coarseBlockMatrix (adaptedCellAtCenter (respGrid jStar F) s w) (respCoeffMinus F a)).upperLeft
(respYMinus P jStar F t e).1)) + √(vecDot (respYMinus P jStar F t e).2
(matVecMul
(coarseBlockMatrix (adaptedCellAtCenter (respGrid jStar F) s w) (respCoeffMinus F a)).lowerRight
(respYMinus P jStar F t e).2))) ^ 2)
P)
(hDint :
MeasureTheory.Integrable
(fun (a : CoeffSpace d) =>
(↑(triadicIndexBox d H).card)⁻¹ * ∑ w ∈ triadicIndexBox d H,
2 * (ResponseJ (adaptedCellAtCenter (respGrid jStar F) s w) (respP (respMean P jStar F t) e)
(respqMinus P jStar F t e) (respCoeffMinus F a) - volumeAverage (adaptedCellAtCenter (respGrid jStar F) s w)
(scalarResponseIntegrand (respCell jStar F t) (respCoeffMinus F a) (respP (respMean P jStar F t) e)
(respqMinus P jStar F t e) (uM a))))
P)
(hMidint :
MeasureTheory.Integrable
(fun (a : CoeffSpace d) =>
√((↑(triadicIndexBox d H).card)⁻¹ * ∑ w ∈ triadicIndexBox d H,
(√(vecDot (respYMinus P jStar F t e).1
(matVecMul
(coarseBlockMatrix (adaptedCellAtCenter (respGrid jStar F) s w) (respCoeffMinus F a)).upperLeft
(respYMinus P jStar F t e).1)) + √(vecDot (respYMinus P jStar F t e).2
(matVecMul
(coarseBlockMatrix (adaptedCellAtCenter (respGrid jStar F) s w) (respCoeffMinus F a)).lowerRight
(respYMinus P jStar F t e).2))) ^ 2) * √((↑(triadicIndexBox d H).card)⁻¹ * ∑ w ∈ triadicIndexBox d H,
2 * (ResponseJ (adaptedCellAtCenter (respGrid jStar F) s w) (respP (respMean P jStar F t) e)
(respqMinus P jStar F t e) (respCoeffMinus F a) - volumeAverage (adaptedCellAtCenter (respGrid jStar F) s w)
(scalarResponseIntegrand (respCell jStar F t) (respCoeffMinus F a) (respP (respMean P jStar F t) e)
(respqMinus P jStar F t e) (uM a)))))
P)
(hPint :
MeasureTheory.Integrable
(fun (a : CoeffSpace d) =>
(↑(triadicIndexBox d H).card)⁻¹ * ∑ w ∈ triadicIndexBox d H,
(volumeAverage (adaptedCellAtCenter (respGrid jStar F) s w) fun (x : Vec d) => φ x - 1) * (√((√(vecDot (respYMinus P jStar F t e).1
(matVecMul
(coarseBlockMatrix (adaptedCellAtCenter (respGrid jStar F) s w)
(respCoeffMinus F a)).upperLeft
(respYMinus P jStar F t e).1)) + √(vecDot (respYMinus P jStar F t e).2
(matVecMul
(coarseBlockMatrix (adaptedCellAtCenter (respGrid jStar F) s w)
(respCoeffMinus F a)).lowerRight
(respYMinus P jStar F t e).2))) ^ 2) * √(2 * (ResponseJ (adaptedCellAtCenter (respGrid jStar F) s w) (respP (respMean P jStar F t) e)
(respqMinus P jStar F t e) (respCoeffMinus F a) - volumeAverage (adaptedCellAtCenter (respGrid jStar F) s w)
(scalarResponseIntegrand (respCell jStar F t) (respCoeffMinus F a)
(respP (respMean P jStar F t) e) (respqMinus P jStar F t e) (uM a))))))
P)
(hPint' :
MeasureTheory.Integrable
(fun (a : CoeffSpace d) =>
(↑(triadicIndexBox d H).card)⁻¹ * ∑ w ∈ triadicIndexBox d H,
(volumeAverage (adaptedCellAtCenter (respGrid jStar F) s w) fun (x : Vec d) => φ x - 1) * (vecDot
(cellAverage (adaptedCellAtCenter (respGrid jStar F) s w) (optimizerField (respCoeffMinus F a) (uM a)) - cellAverage (adaptedCellAtCenter (respGrid jStar F) s w)
(optimizerField (respCoeffMinus F a) (v w a))).1
(respYMinus P jStar F t e).2 + vecDot (respYMinus P jStar F t e).1
(cellAverage (adaptedCellAtCenter (respGrid jStar F) s w) (optimizerField (respCoeffMinus F a) (uM a)) - cellAverage (adaptedCellAtCenter (respGrid jStar F) s w)
(optimizerField (respCoeffMinus F a) (v w a))).2))
P)
(hmeasBlk :
∀ (α β : BlockCoord d),
MeasureTheory.AEStronglyMeasurable
(fun (a : CoeffSpace d) =>
blockMatEntry (coarseBlockMatrix (adaptedCell (respGrid jStar F) s) (respCoeffMinus F a)) α β)
P)
(hintM1 :
∀ w ∈ triadicIndexBox d H,
∀ (i : Fin d),
MeasureTheory.Integrable
(fun (a : CoeffSpace d) =>
(cellAverage (adaptedCellAtCenter (respGrid jStar F) s w) (optimizerField (respCoeffMinus F a) (uM a))).1 i)
P)
(hintM2 :
∀ w ∈ triadicIndexBox d H,
∀ (i : Fin d),
MeasureTheory.Integrable
(fun (a : CoeffSpace d) =>
(cellAverage (adaptedCellAtCenter (respGrid jStar F) s w) (optimizerField (respCoeffMinus F a) (uM a))).2 i)
P)
(hintNs1 :
∀ w ∈ triadicIndexBox d H,
∀ (i : Fin d),
MeasureTheory.Integrable
(fun (a : CoeffSpace d) =>
(cellAverage (adaptedCellAtCenter (respGrid jStar F) s w) (optimizerField (respCoeffMinus F a) (v w a))).1 i)
P)
(hintNs2 :
∀ w ∈ triadicIndexBox d H,
∀ (i : Fin d),
MeasureTheory.Integrable
(fun (a : CoeffSpace d) =>
(cellAverage (adaptedCellAtCenter (respGrid jStar F) s w) (optimizerField (respCoeffMinus F a) (v w a))).2 i)
P)
(Ncell : BlockVec d)
(hNcell :
Ncell = (fun (i : Fin d) =>
∫ (a : CoeffSpace d), (↑(triadicIndexBox d H).card)⁻¹ * ∑ w ∈ triadicIndexBox d H,
(volumeAverage (adaptedCellAtCenter (respGrid jStar F) s w) fun (x : Vec d) => φ x - 1) * volumeAverage (adaptedCellAtCenter (respGrid jStar F) s w) fun (x : Vec d) =>
(optimizerField (respCoeffMinus F a) (uM a) x).1 i ∂P, fun (i : Fin d) =>
∫ (a : CoeffSpace d), (↑(triadicIndexBox d H).card)⁻¹ * ∑ w ∈ triadicIndexBox d H,
(volumeAverage (adaptedCellAtCenter (respGrid jStar F) s w) fun (x : Vec d) => φ x - 1) * volumeAverage (adaptedCellAtCenter (respGrid jStar F) s w) fun (x : Vec d) =>
(optimizerField (respCoeffMinus F a) (uM a) x).2 i ∂P))
:
|vecDot Ncell.1 (respYMinus P jStar F t e).2 + vecDot (respYMinus P jStar F t e).1 Ncell.2| ≤ √(respLsMinus P jStar F s t e) * √(2 * respTauMinus P jStar F s t e)
The cell half of the cutoff-mean row on the carriers, minus sign. Let Ncell be the cell
part of the cutoff-mean defect of p.response.transfer produced by the centred cutoff
decomposition of the terminal optimizer state of the recentred coefficient a_- = a - g, namely
the weighted flat average over the depth-H subcells of the subcell mean of φ - 1 times the
subcell mean of the doubled optimizer field. Then the modulus of the crossed pairing of Ncell
against the dual variable Y^- is at most √(L_s^-) * √(2 tau^-). The proof runs the abstract
cell-pairing row at the concrete crossing of the difference between the terminal and subcell
optimizer means, discharges its pathwise bound by the direct full-dual pairing estimate, discharges
its deficit value by the rescaling of the mean subcell deficit, and rewrites its flat average back
to Ncell with the crossed-pairing linearity and the cancellation of the constant cell means.
theorem
HCPolySupport.HighContrast.Multiscale.abs_vecDot_cellPart_respYPlus_le
{d : ℕ}
[NeZero d]
(P : MeasureTheory.Measure (CoeffSpace d))
[MeasureTheory.IsProbabilityMeasure P]
(hstat : IsStationaryLaw P)
(jStar : ℕ)
(hjStar : 2 * d ≤ 3 ^ jStar)
(F : BlockMat d)
(hm : Matrix.PosDef (explicitCanonicalMetric F))
(H : ℕ)
(s t : ℤ)
(ht : t = s + ↑H)
(hjs : ↑jStar ≤ s)
(e : Vec d)
(φ : Vec d → ℝ)
(hφ : IsResponseCutoff (respGrid jStar F) t φ)
(uP : (a : CoeffSpace d) → AHarmonicFunction (respCoeffPlus F a) (respCell jStar F t))
(hmax :
∀ (a : CoeffSpace d),
IsResponseMaximizer (respCell jStar F t) (respP (respMean P jStar F t) e) (respqPlus P jStar F t e)
(respCoeffPlus F a) (uP a))
(v :
(w : Fin d → ℤ) →
(a : CoeffSpace d) → AHarmonicFunction (respCoeffPlus F a) (adaptedCellAtCenter (respGrid jStar F) s w))
(hmaxV :
∀ w ∈ triadicIndexBox d H,
∀ (a : CoeffSpace d),
IsResponseMaximizer (adaptedCellAtCenter (respGrid jStar F) s w) (respP (respMean P jStar F t) e)
(respqPlus P jStar F t e) (respCoeffPlus F a) (v w a))
(hsum : Summable (respSourceLoadSummand P jStar F s (respCoeffPlus F) (respYPlus P jStar F t e)))
(hblk : ∀ (w : Fin d → ℤ), HasIntegrableCoarseBlock P (adaptedCellAtCenter (respGrid jStar F) s w))
(hrespint :
∀ (a : CoeffSpace d),
MeasureTheory.IntegrableOn
(scalarResponseIntegrand (respCell jStar F t) (respCoeffPlus F a) (respP (respMean P jStar F t) e)
(respqPlus P jStar F t e) (uP a))
(respCell jStar F t) MeasureTheory.volume)
(hJint :
∀ w ∈ triadicIndexBox d H,
MeasureTheory.Integrable
(fun (a : CoeffSpace d) =>
ResponseJ (adaptedCellAtCenter (respGrid jStar F) s w) (respP (respMean P jStar F t) e)
(respqPlus P jStar F t e) (respCoeffPlus F a))
P)
(hRint :
∀ w ∈ triadicIndexBox d H,
MeasureTheory.Integrable
(fun (a : CoeffSpace d) =>
volumeAverage (adaptedCellAtCenter (respGrid jStar F) s w)
(scalarResponseIntegrand (respCell jStar F t) (respCoeffPlus F a) (respP (respMean P jStar F t) e)
(respqPlus P jStar F t e) (uP a)))
P)
(hJt :
MeasureTheory.Integrable
(fun (a : CoeffSpace d) =>
respJ (respGrid jStar F) t (respP (respMean P jStar F t) e) (respqPlus P jStar F t e) (respCoeffPlus F a))
P)
(hJs :
MeasureTheory.Integrable
(fun (a : CoeffSpace d) =>
respJ (respGrid jStar F) s (respP (respMean P jStar F t) e) (respqPlus P jStar F t e) (respCoeffPlus F a))
P)
(hUL :
∀ w ∈ triadicIndexBox d H,
∀ (a : CoeffSpace d),
0 ≤ vecDot (respYPlus P jStar F t e).1
(matVecMul (coarseBlockMatrix (adaptedCellAtCenter (respGrid jStar F) s w) (respCoeffPlus F a)).upperLeft
(respYPlus P jStar F t e).1))
(hLR :
∀ w ∈ triadicIndexBox d H,
∀ (a : CoeffSpace d),
0 ≤ vecDot (respYPlus P jStar F t e).2
(matVecMul (coarseBlockMatrix (adaptedCellAtCenter (respGrid jStar F) s w) (respCoeffPlus F a)).lowerRight
(respYPlus P jStar F t e).2))
(hentUL :
∀ w ∈ triadicIndexBox d H,
∀ (i j : Fin d),
MeasureTheory.Integrable
(fun (a : CoeffSpace d) =>
(coarseBlockMatrix (adaptedCellAtCenter (respGrid jStar F) s w) (respCoeffPlus F a)).upperLeft i j)
P)
(hentLR :
∀ w ∈ triadicIndexBox d H,
∀ (i j : Fin d),
MeasureTheory.Integrable
(fun (a : CoeffSpace d) =>
(coarseBlockMatrix (adaptedCellAtCenter (respGrid jStar F) s w) (respCoeffPlus F a)).lowerRight i j)
P)
(hqUL :
∀ w ∈ triadicIndexBox d H,
MeasureTheory.Integrable
(fun (a : CoeffSpace d) =>
vecDot (respYPlus P jStar F t e).1
(matVecMul (coarseBlockMatrix (adaptedCellAtCenter (respGrid jStar F) s w) (respCoeffPlus F a)).upperLeft
(respYPlus P jStar F t e).1))
P)
(hqLR :
∀ w ∈ triadicIndexBox d H,
MeasureTheory.Integrable
(fun (a : CoeffSpace d) =>
vecDot (respYPlus P jStar F t e).2
(matVecMul (coarseBlockMatrix (adaptedCellAtCenter (respGrid jStar F) s w) (respCoeffPlus F a)).lowerRight
(respYPlus P jStar F t e).2))
P)
(hcross :
∀ w ∈ triadicIndexBox d H,
MeasureTheory.Integrable
(fun (a : CoeffSpace d) =>
√(vecDot (respYPlus P jStar F t e).1
(matVecMul (coarseBlockMatrix (adaptedCellAtCenter (respGrid jStar F) s w) (respCoeffPlus F a)).upperLeft
(respYPlus P jStar F t e).1)) * √(vecDot (respYPlus P jStar F t e).2
(matVecMul (coarseBlockMatrix (adaptedCellAtCenter (respGrid jStar F) s w) (respCoeffPlus F a)).lowerRight
(respYPlus P jStar F t e).2)))
P)
(hsq :
∀ w ∈ triadicIndexBox d H,
MeasureTheory.Integrable
(fun (a : CoeffSpace d) =>
(√(vecDot (respYPlus P jStar F t e).1
(matVecMul
(coarseBlockMatrix (adaptedCellAtCenter (respGrid jStar F) s w) (respCoeffPlus F a)).upperLeft
(respYPlus P jStar F t e).1)) + √(vecDot (respYPlus P jStar F t e).2
(matVecMul
(coarseBlockMatrix (adaptedCellAtCenter (respGrid jStar F) s w) (respCoeffPlus F a)).lowerRight
(respYPlus P jStar F t e).2))) ^ 2)
P)
(hFint :
MeasureTheory.Integrable
(fun (a : CoeffSpace d) =>
(↑(triadicIndexBox d H).card)⁻¹ * ∑ w ∈ triadicIndexBox d H,
(√(vecDot (respYPlus P jStar F t e).1
(matVecMul
(coarseBlockMatrix (adaptedCellAtCenter (respGrid jStar F) s w) (respCoeffPlus F a)).upperLeft
(respYPlus P jStar F t e).1)) + √(vecDot (respYPlus P jStar F t e).2
(matVecMul
(coarseBlockMatrix (adaptedCellAtCenter (respGrid jStar F) s w) (respCoeffPlus F a)).lowerRight
(respYPlus P jStar F t e).2))) ^ 2)
P)
(hDint :
MeasureTheory.Integrable
(fun (a : CoeffSpace d) =>
(↑(triadicIndexBox d H).card)⁻¹ * ∑ w ∈ triadicIndexBox d H,
2 * (ResponseJ (adaptedCellAtCenter (respGrid jStar F) s w) (respP (respMean P jStar F t) e)
(respqPlus P jStar F t e) (respCoeffPlus F a) - volumeAverage (adaptedCellAtCenter (respGrid jStar F) s w)
(scalarResponseIntegrand (respCell jStar F t) (respCoeffPlus F a) (respP (respMean P jStar F t) e)
(respqPlus P jStar F t e) (uP a))))
P)
(hMidint :
MeasureTheory.Integrable
(fun (a : CoeffSpace d) =>
√((↑(triadicIndexBox d H).card)⁻¹ * ∑ w ∈ triadicIndexBox d H,
(√(vecDot (respYPlus P jStar F t e).1
(matVecMul
(coarseBlockMatrix (adaptedCellAtCenter (respGrid jStar F) s w) (respCoeffPlus F a)).upperLeft
(respYPlus P jStar F t e).1)) + √(vecDot (respYPlus P jStar F t e).2
(matVecMul
(coarseBlockMatrix (adaptedCellAtCenter (respGrid jStar F) s w) (respCoeffPlus F a)).lowerRight
(respYPlus P jStar F t e).2))) ^ 2) * √((↑(triadicIndexBox d H).card)⁻¹ * ∑ w ∈ triadicIndexBox d H,
2 * (ResponseJ (adaptedCellAtCenter (respGrid jStar F) s w) (respP (respMean P jStar F t) e)
(respqPlus P jStar F t e) (respCoeffPlus F a) - volumeAverage (adaptedCellAtCenter (respGrid jStar F) s w)
(scalarResponseIntegrand (respCell jStar F t) (respCoeffPlus F a) (respP (respMean P jStar F t) e)
(respqPlus P jStar F t e) (uP a)))))
P)
(hPint :
MeasureTheory.Integrable
(fun (a : CoeffSpace d) =>
(↑(triadicIndexBox d H).card)⁻¹ * ∑ w ∈ triadicIndexBox d H,
(volumeAverage (adaptedCellAtCenter (respGrid jStar F) s w) fun (x : Vec d) => φ x - 1) * (√((√(vecDot (respYPlus P jStar F t e).1
(matVecMul
(coarseBlockMatrix (adaptedCellAtCenter (respGrid jStar F) s w) (respCoeffPlus F a)).upperLeft
(respYPlus P jStar F t e).1)) + √(vecDot (respYPlus P jStar F t e).2
(matVecMul
(coarseBlockMatrix (adaptedCellAtCenter (respGrid jStar F) s w)
(respCoeffPlus F a)).lowerRight
(respYPlus P jStar F t e).2))) ^ 2) * √(2 * (ResponseJ (adaptedCellAtCenter (respGrid jStar F) s w) (respP (respMean P jStar F t) e)
(respqPlus P jStar F t e) (respCoeffPlus F a) - volumeAverage (adaptedCellAtCenter (respGrid jStar F) s w)
(scalarResponseIntegrand (respCell jStar F t) (respCoeffPlus F a) (respP (respMean P jStar F t) e)
(respqPlus P jStar F t e) (uP a))))))
P)
(hPint' :
MeasureTheory.Integrable
(fun (a : CoeffSpace d) =>
(↑(triadicIndexBox d H).card)⁻¹ * ∑ w ∈ triadicIndexBox d H,
(volumeAverage (adaptedCellAtCenter (respGrid jStar F) s w) fun (x : Vec d) => φ x - 1) * (vecDot
(cellAverage (adaptedCellAtCenter (respGrid jStar F) s w) (optimizerField (respCoeffPlus F a) (uP a)) - cellAverage (adaptedCellAtCenter (respGrid jStar F) s w)
(optimizerField (respCoeffPlus F a) (v w a))).1
(respYPlus P jStar F t e).2 + vecDot (respYPlus P jStar F t e).1
(cellAverage (adaptedCellAtCenter (respGrid jStar F) s w) (optimizerField (respCoeffPlus F a) (uP a)) - cellAverage (adaptedCellAtCenter (respGrid jStar F) s w)
(optimizerField (respCoeffPlus F a) (v w a))).2))
P)
(hmeasBlk :
∀ (α β : BlockCoord d),
MeasureTheory.AEStronglyMeasurable
(fun (a : CoeffSpace d) =>
blockMatEntry (coarseBlockMatrix (adaptedCell (respGrid jStar F) s) (respCoeffPlus F a)) α β)
P)
(hintM1 :
∀ w ∈ triadicIndexBox d H,
∀ (i : Fin d),
MeasureTheory.Integrable
(fun (a : CoeffSpace d) =>
(cellAverage (adaptedCellAtCenter (respGrid jStar F) s w) (optimizerField (respCoeffPlus F a) (uP a))).1 i)
P)
(hintM2 :
∀ w ∈ triadicIndexBox d H,
∀ (i : Fin d),
MeasureTheory.Integrable
(fun (a : CoeffSpace d) =>
(cellAverage (adaptedCellAtCenter (respGrid jStar F) s w) (optimizerField (respCoeffPlus F a) (uP a))).2 i)
P)
(hintNs1 :
∀ w ∈ triadicIndexBox d H,
∀ (i : Fin d),
MeasureTheory.Integrable
(fun (a : CoeffSpace d) =>
(cellAverage (adaptedCellAtCenter (respGrid jStar F) s w) (optimizerField (respCoeffPlus F a) (v w a))).1 i)
P)
(hintNs2 :
∀ w ∈ triadicIndexBox d H,
∀ (i : Fin d),
MeasureTheory.Integrable
(fun (a : CoeffSpace d) =>
(cellAverage (adaptedCellAtCenter (respGrid jStar F) s w) (optimizerField (respCoeffPlus F a) (v w a))).2 i)
P)
(Ncell : BlockVec d)
(hNcell :
Ncell = (fun (i : Fin d) =>
∫ (a : CoeffSpace d), (↑(triadicIndexBox d H).card)⁻¹ * ∑ w ∈ triadicIndexBox d H,
(volumeAverage (adaptedCellAtCenter (respGrid jStar F) s w) fun (x : Vec d) => φ x - 1) * volumeAverage (adaptedCellAtCenter (respGrid jStar F) s w) fun (x : Vec d) =>
(optimizerField (respCoeffPlus F a) (uP a) x).1 i ∂P, fun (i : Fin d) =>
∫ (a : CoeffSpace d), (↑(triadicIndexBox d H).card)⁻¹ * ∑ w ∈ triadicIndexBox d H,
(volumeAverage (adaptedCellAtCenter (respGrid jStar F) s w) fun (x : Vec d) => φ x - 1) * volumeAverage (adaptedCellAtCenter (respGrid jStar F) s w) fun (x : Vec d) =>
(optimizerField (respCoeffPlus F a) (uP a) x).2 i ∂P))
:
The cell half of the cutoff-mean row on the carriers, plus sign. The adjoint twin of
abs_vecDot_cellPart_respYMinus_le: Ncell is the cell part of the cutoff-mean defect for the
adjoint recentred coefficient a_+ = aᵗ + g, built from the terminal optimizer family uP, and the
modulus of its crossed pairing against Y^+ is at most √(L_s^+) * √(2 tau^+). The proof is the
same as for the minus sign, with the adjoint per-cell pairing bound, the adjoint deficit rescaling
and the adjoint mean cancellation.