High-contrast homogenization: Provider.Entry.AdapterCellRows

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

The rows of the Euclidean filling of an adapted cell

The pathwise rows majorant. The rows of a finite range of generations are kept whole and only the tail below an arbitrary cutoff is paid crudely; this is the form the averaging of e.two.grid.whitney.average consumes. Only the tail below the cutoff is paid crudely, in the majorant of AdapterMajorant.

There are no definitions in this file.

theorem HCPolySupport.HighContrast.Entry.ae_coarseBlock_adaptedCellTranslate_le_rows {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} {g : ℝ} {E : BlockMat d} {Ψ : ℝ → ℝ} {K : ℝ} {S : CoeffSpace d → ℝ} (hdag : CoarseEllipticityDagger P g E Ψ K S) {q : Mat d} (hq : Matrix.PosDef q) {nn M J : ℤ} {y : Vec d} (hM : 0 ≤ M) (hJn : J ≤ nn) (hMsub : adaptedCellTranslate q nn y ⊆ centeredCube d M) {Z : ℤ → Finset (Fin d → ℤ)} (hZ : ∀ (s : ℤ), ↑(Z s) = Transport.fillingIndex 1 nn (adaptedCellTranslate q nn y) s) : ∀ᵐ (a : CoeffSpace d) ∂P, toFullBlockMat (coarseBlock (adaptedCellTranslate q nn y) a) ≤ ∑ r ∈ Finset.Icc J nn, ∑ w ∈ Z r, ((MeasureTheory.volume (adaptedCellAt 1 r w)).toReal / (MeasureTheory.volume (adaptedCellTranslate q nn y)).toReal) • toFullBlockMat (coarseBlock (adaptedCellAt 1 r w) a) + (6 * ↑d * √↑d * ‖q⁻¹‖ * (2 * (1 - g)⁻¹ * (3 ^ J + 3 ^ M + 3 * S a) * (3 ^ (-nn) * 3 ^ (↑J * (1 - g))))) • toFullBlockMat E

The pathwise majorant of the Euclidean filling of a translated adapted cell. The coarse response of the target lies below the weighted rows of the filling from an arbitrary cutoff up to the starting generation, plus the crude tail of AdapterMajorant, whose coefficient is affine in the source scale.