High-contrast homogenization: Entry.Response.Kernel.ResponseFieldSize

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

The size of a recentred response field

This file bounds the metric size of a doubled cell average by the cell energy, given a doubled response field Y and the two size hypotheses that relate it to the normalized block: it shows the normalized block is Hermitian, bounds it by one plus the spectral bound, and controls the metric of the recent-scale difference by the weighted all-scale maximum. It also compares the pointwise selection Nonempty.some of a response maximizer with the Chapter-2 canonical maximizer, showing their gradients, fluxes and subcell averages of the doubled state agree almost everywhere, and records the measurability of the resulting coefficient carriers.

The results below are the response-field size, restriction and selection steps of the response-transfer estimate p.response.transfer.

The response field of a recentred difference, and its size

diagonalWeakNorm_primal_le (DiagonalWeakNormBound.lean) is untouched: nothing here restates, weakens or deletes any existing declaration.

What this module supplies

The metric size of a doubled cell average is reduced to the cell energy (SharpOrderEnergyMap.lean), given a doubled RESPONSE FIELD Y and two size inequalities. That reduction leaves open exactly two inputs:

1. the Y CONSTRUCTION for the recentred DIFFERENCE field, isDoubledResponseField_grad_sub; and
2. the RESPONSE-SIZE step, the hsize bound of diagonalWeak_recent_average_bound, fed by sqrt_blockSize_adaptedResponse_le_of_maximum_finite.

Both isDoubledResponseField_grad_sub and exists_restrict_solution_adaptedCellAtCenter are supplied here.

The size inputs are Loewner bounds

blockSize, adaptedResponse, metricBlockNormSq, relSize and blockSharp are not defined on this tree. The block-size inequality blockSize A E ≤ B² is written here as the LOEWNER inequality toFullBlockMat A ≤ B² • toFullBlockMat E, which is the shape the size input hAE actually takes, and blockExcess A E is written as the block spectral bound blockSpecBound (blockSub (normalizedBlock A E) (blockIdentity d)) — the quantity respAllScaleMax (ResponseBlockObjects.lean) is already built from. That substitution removes the blockSize_le_one_add_blockExcess step altogether, and with it the blockSpecBound-subadditivity obstruction recorded in RecentHeadDefectHalves.lean: the recentring bound N ≤ (1 + β) I is read straight off blockMatLoewnerLE_blockScale_blockSpecBound_self (RecentScaleEnergyRoute.lean), with no operator norm anywhere.

This module introduces exactly ONE definition, adaptedDomainAt, and it selects no constant: it is the per-w Chapter-2 domain whose carrier is adaptedCellAtCenter q (t-n) w, and its two structure obligations are discharged inside the definition itself from isOpenBoundedConvexDomain_adaptedCellAtCenter (DiagonalDefectCarriers.lean) and volume_adaptedCellAtCenter_toReal_pos (…:293). Its satisfiability is nevertheless exhibited as an explicit ∃ before any consumer statement. Every other declaration below is a theorem.

The cellAverage/averageVec bridge is definitional

cellAverage V X (ResponseBlockObjects.lean) and the pair (Book.Ch02.averageVec U Y.potential, Book.Ch02.averageVec U Y.flux) are the same term: volumeAverage (CG CoarseGraining/Definitions.lean) and Book.Ch02.average (CG Book/Ch02/Response.lean) have identical bodies. Two rfl lemmas record this, so the response-size step costs two lines, not a lemma.

The doubled response field of a difference of solutions

The Y construction for the recentred difference field, stated on CoarseGraining's carriers.

The carrier bridge is definitional

The recentred-difference energy map on this tree's carriers

theorem HCPolySupport.HighContrast.Multiscale.recent_difference_metric_le {d : ℕ} {U : Book.Ch02.Domain d} {a : Book.Ch02.CoeffOn U} (hEll : IsEllipticFieldOn a.lam a.Lam U.carrier a.toCoeffField) (u v : Book.Ch02.Solution U a) {F : BlockMat d} (hm : Matrix.PosDef (explicitCanonicalMetric F)) {E : BlockMat d} (hE : Matrix.PosDef (toFullBlockMat E)) {k e : ℝ} (hk : 0 < k) (he : 0 < e) (hEM : toFullBlockMat E ≤ k • toFullBlockMat (respM0 F)) (hAE : toFullBlockMat (Book.Ch02.coarseBlockMatrix U a) ≤ e • toFullBlockMat E) : blockVecDot (blockMatVecMul (blockSqrt (respM0 F)) (cellAverage U.carrier fun (x : Vec d) => optimizerField a.toCoeffField u x - optimizerField a.toCoeffField v x)) (blockMatVecMul (blockSqrt (respM0 F)) (cellAverage U.carrier fun (x : Vec d) => optimizerField a.toCoeffField u x - optimizerField a.toCoeffField v x)) ≤ k * e * Book.Ch02.average U fun (x : Vec d) => blockVecDot (optimizerField a.toCoeffField u x - optimizerField a.toCoeffField v x) (blockMatVecMul (Book.Ch02.blockMatrixField a x) (optimizerField a.toCoeffField u x - optimizerField a.toCoeffField v x))

The recentred-difference energy map. The R-metric size of the cell average of the doubled difference of two optimizers is controlled by the cell energy of that difference, with constant k · e given the two size inputs.

Three deliberate strengthenings:

• the domain is an ARBITRARY U : Domain d, not adaptedDomainAt hq k w, so the statement carries no geometry at all (the child cell can be supplied when a consumer wants it);
• diagonalWeakMetricFactor m E ^ 2 * blockSize (adaptedResponse q k w a) E is replaced by the two Loewner inputs hEM, hAE with arbitrary positive k, e — a BOUND on the size, not the size, which is the shape a consumer owns;
• the Solution.ofAEEq/exists_pointwise_coeffOn_family_aeeq preamble is NOT reproduced: it moves the sample a to an elliptic representative c, and this tree already carries that move separately (cellAverage_optimizerField_respCoeffMinus_eq_at, DiagonalDefectCarriers.lean). The statement below is at the representative, so the two moves compose without duplication.

The RESPONSE-SIZE step

The bound blockSize (adaptedResponse q k w a) E ≤ B², written as the Loewner inequality that the size input hAE actually takes.

theorem HCPolySupport.HighContrast.Multiscale.isHermitian_normalizedBlock {d : ℕ} {P Q : BlockMat d} (hP : Matrix.IsHermitian (toFullBlockMat P)) (hQ : Matrix.PosDef (toFullBlockMat Q)) : Matrix.IsHermitian (toFullBlockMat (normalizedBlock P Q))

The normalized block of a Hermitian block by a positive definite reference is Hermitian. E^{-1/2} is symmetric, so the congruence preserves symmetry.

theorem HCPolySupport.HighContrast.Multiscale.normalizedBlock_le_one_add_specBound {d : ℕ} {N : BlockMat d} (hN : Matrix.IsHermitian (toFullBlockMat N)) : toFullBlockMat N ≤ (1 + blockSpecBound (blockSub N (Book.Ch02.blockIdentity d))) • 1

The recentring step, with NO operator norm. A Hermitian doubled block is dominated by (1 + β) I, where β is the spectral positive part of its recentring N - I:

N ≤ (1 + β) · I_{2d}, β = blockSpecBound (N - I).

This replaces blockSize_le_one_add_blockExcess, which goes through the norm and therefore needs blockSpecBound subadditivity — the obstruction recorded at RecentHeadDefectHalves.lean. Here blockMatLoewnerLE_blockScale_blockSpecBound_self (RecentScaleEnergyRoute.lean) gives the Loewner bound on N - I directly and the identity is added back on quadratic forms, so no norm and no subadditivity is used.

theorem HCPolySupport.HighContrast.Multiscale.le_smul_of_normalizedBlock_le {d : ℕ} {P Q : BlockMat d} {c : ℝ} (hQ : Matrix.PosDef (toFullBlockMat Q)) (hc : toFullBlockMat (normalizedBlock P Q) ≤ c • 1) : toFullBlockMat P ≤ c • toFullBlockMat Q

A bound on the normalized block against the identity lifts back to a bound of the block against its reference: E^{-1/2} P E^{-1/2} ≤ c I ⟹ P ≤ c E. This is the tail of SharpOrderEnergyMap.lean with the operator norm replaced by an arbitrary constant, which is what a consumer owning only a BOUND has.

theorem HCPolySupport.HighContrast.Multiscale.le_smul_of_specBound_le {d : ℕ} {Z E : BlockMat d} {c : ℝ} (hZ : Matrix.IsHermitian (toFullBlockMat Z)) (hE : Matrix.PosDef (toFullBlockMat E)) (hc : 1 + blockSpecBound (blockSub (normalizedBlock Z E) (Book.Ch02.blockIdentity d)) ≤ c) : toFullBlockMat Z ≤ c • toFullBlockMat E

The size step, carrier-free. Z ≤ c E as soon as c dominates 1 + blockSpecBound (normalizedBlock Z E - I). This is exactly the bound blockSize A E ≤ B² once blockSize is read as a Loewner bound rather than as a norm.

theorem HCPolySupport.HighContrast.Multiscale.one_add_le_sq {x B : ℝ} (hx : 0 ≤ x) (hB : √x ≤ B - 1) : 1 + x ≤ B ^ 2

1 + x ≤ B² whenever √x ≤ B - 1. The squaring bookkeeping of the response-size step, on bare reals.

theorem HCPolySupport.HighContrast.Multiscale.blockCongr_le_smul {d : ℕ} {Z E : BlockMat d} (G : BlockMat d) {c : ℝ} (h : toFullBlockMat Z ≤ c • toFullBlockMat E) : toFullBlockMat (blockCongr G Z) ≤ c • toFullBlockMat (blockCongr G E)

Congruence transfer of a Loewner size bound. Z ≤ c E gives GᵀZG ≤ c GᵀEG for ANY G: no positive definiteness, no invertibility, no symmetry.

This is the step that carries a bound stated in the respMean picture, which is where respAllScaleMax (ResponseBlockObjects.lean) lives, into the respEhatMinus picture, which is where the size input hAE lives, since respEhatMinus = blockCongr (respG F) (respMean …) (ResponseBlockObjects.lean). The equality h6a_blockOpNorm_recentred_blockCongr_eq CANNOT be used for this transfer, because it is an equality of OPERATOR NORMS while respAllScaleMax carries a blockSpecBound, and blockSpecBound ≤ ‖·‖ points the wrong way.

theorem HCPolySupport.HighContrast.Multiscale.weighted_specBound_le_respAllScaleMax {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (γ : ℝ) (jStar : ℕ) (F : BlockMat d) (t : ℤ) (a : CoeffSpace d) (n : ℕ) {w : Fin d → ℤ} (hw : w ∈ triadicIndexBox d n) (hbdd : BddAbove {y : ℝ | ∃ (m : ℕ), ∃ z ∈ triadicIndexBox d m, y = 3 ^ (-(Quenched.contrastRho γ * ↑m)) * blockSpecBound (blockSub (normalizedBlock (coarseBlock (adaptedCellAtCenter (respGrid jStar F) (t - ↑m) z) a) (respMean P jStar F t)) (Book.Ch02.blockIdentity d))}) : 3 ^ (-(Quenched.contrastRho γ * ↑n)) * blockSpecBound (blockSub (normalizedBlock (coarseBlock (adaptedCellAtCenter (respGrid jStar F) (t - ↑n) w) a) (respMean P jStar F t)) (Book.Ch02.blockIdentity d)) ≤ respAllScaleMax P γ jStar F t a

Every weighted cell excess is bounded by the all-scale maximum, on the branch where that supremum is finite. This is weighted_excess_le_diagonalWeakMaximum_toReal, whose finiteness hypothesis hfinite : diagonalWeakMaximum … ≠ ⊤ is here the real-valued BddAbove of the same set (this tree's respAllScaleMax is an sSup in ℝ, not in ℝ≥0∞).

The response-size step, assembled on the tree's own carriers

theorem HCPolySupport.HighContrast.Multiscale.coarseBlock_le_sq_smul_respMean {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (γ : ℝ) (jStar : ℕ) (F : BlockMat d) (t : ℤ) (a : CoeffSpace d) (n : ℕ) {w : Fin d → ℤ} (hw : w ∈ triadicIndexBox d n) (hbdd : BddAbove {y : ℝ | ∃ (m : ℕ), ∃ z ∈ triadicIndexBox d m, y = 3 ^ (-(Quenched.contrastRho γ * ↑m)) * blockSpecBound (blockSub (normalizedBlock (coarseBlock (adaptedCellAtCenter (respGrid jStar F) (t - ↑m) z) a) (respMean P jStar F t)) (Book.Ch02.blockIdentity d))}) (hE : Matrix.PosDef (toFullBlockMat (respMean P jStar F t))) : toFullBlockMat (coarseBlock (adaptedCellAtCenter (respGrid jStar F) (t - ↑n) w) a) ≤ (1 + √(respAllScaleMax P γ jStar F t a) * 3 ^ (Quenched.contrastRho γ * ↑n / 2)) ^ 2 • toFullBlockMat (respMean P jStar F t)

THE RESPONSE-SIZE STEP, in the respMean picture. The coarse response of an aligned child cell sits below the scale-t reference mean, dilated by the square of the printed geometric weight:

𝐀(z + U_{t-n}; a) ≤ (1 + √M · 3^{ρn/2})² · E_t, M = respAllScaleMax P γ jStar F t a.

This is the hsize bound of diagonalWeak_recent_average_bound, fed by sqrt_blockSize_adaptedResponse_le_of_maximum_finite. The bound blockSize (adaptedResponse q k w a) E is the Loewner statement here; blockExcess is the blockSpecBound of the recentred normalized block, the very quantity respAllScaleMax (ResponseBlockObjects.lean) is built from, so no excess carrier is needed either. sqrt_le_sqrt_mul_rpow_of_weighted_le (RecentHeadDefectHalves.lean) supplies the geometric-weight arithmetic, already in this tree.

theorem HCPolySupport.HighContrast.Multiscale.coarseBlock_congr_le_sq_smul_respEhatMinus {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (γ : ℝ) (jStar : ℕ) (F : BlockMat d) (t : ℤ) (a : CoeffSpace d) (n : ℕ) {w : Fin d → ℤ} (hw : w ∈ triadicIndexBox d n) (hbdd : BddAbove {y : ℝ | ∃ (m : ℕ), ∃ z ∈ triadicIndexBox d m, y = 3 ^ (-(Quenched.contrastRho γ * ↑m)) * blockSpecBound (blockSub (normalizedBlock (coarseBlock (adaptedCellAtCenter (respGrid jStar F) (t - ↑m) z) a) (respMean P jStar F t)) (Book.Ch02.blockIdentity d))}) (hE : Matrix.PosDef (toFullBlockMat (respMean P jStar F t))) : toFullBlockMat (blockCongr (respG F) (coarseBlock (adaptedCellAtCenter (respGrid jStar F) (t - ↑n) w) a)) ≤ (1 + √(respAllScaleMax P γ jStar F t a) * 3 ^ (Quenched.contrastRho γ * ↑n / 2)) ^ 2 • toFullBlockMat (respEhatMinus P jStar F t)

THE RESPONSE-SIZE STEP, in the Ehat^- picture. The previous bound, conjugated by the shear G(F), which is exactly the passage from respMean to respEhatMinus = blockCongr (respG F) (respMean …) (ResponseBlockObjects.lean).

A consumer closes the size input hAE from this by identifying its numerator: the coarse block of the recentred field, Book.Ch02.coarseBlockMatrix U (respCoeffMinus F a), is blockCongr (respG F) (coarseBlock U a) — the shear identity coarseBlockMatrix_sub_skew_eq_blockCongr (HCPoly/Entry/Response/Core/SkewShearCongruence.lean, and not restated here).

The restriction step, and the per-w child cell as a Chapter-2 domain

The restriction step supplies exists_restrict_solution and exists_restrict_solution_adaptedCellAtCenter. A consumer needs them to produce the SECOND argument of the recentred-difference energy map: the parent optimizer, restricted to the child cell.

theorem HCPolySupport.HighContrast.Multiscale.adaptedCellAtCenter_nonempty_of_isUnit_of_neZero {d : ℕ} (q : Mat d) (hq : IsUnit q) (k : ℤ) (w : Fin d → ℤ) : (adaptedCellAtCenter q k w).Nonempty

An aligned adapted cell is nonempty. This is proved from the PUBLIC volume_adaptedCellAtCenter_toReal_pos (DiagonalDefectCarriers.lean), mirroring the private adaptedCellAtCenter_nonempty (…:366).

def HCPolySupport.HighContrast.Multiscale.adaptedDomainAt {d : ℕ} (q : Mat d) (hq : IsUnit q) (k : ℤ) (w : Fin d → ℤ) : Book.Ch02.Domain d

The ONLY definition in this module. The aligned adapted cell z + q□_k as a Chapter-2 domain, the per-w twin of adaptedDomain.

This definition selects NO constant and carries no inequality of its own: its two structure obligations are Props about the carrier adaptedCellAtCenter q k w, and both are discharged inside the definition itself, from isOpenBoundedConvexDomain_adaptedCellAtCenter (DiagonalDefectCarriers.lean, PUBLIC) and the nonemptiness proved above. Its satisfiability is therefore constructive; it is nevertheless exhibited as an explicit ∃, before any consumer.

Equations

• HCPolySupport.HighContrast.Multiscale.adaptedDomainAt q hq k w = { carrier := HCPolySupport.HighContrast.adaptedCellAtCenter q k w, isDomain := ⋯, nonempty := ⋯ }

@[simp]

theorem HCPolySupport.HighContrast.Multiscale.adaptedDomainAt_carrier {d : ℕ} (q : Mat d) (hq : IsUnit q) (k : ℤ) (w : Fin d → ℤ) : (adaptedDomainAt q hq k w).carrier = adaptedCellAtCenter q k w

theorem HCPolySupport.HighContrast.Multiscale.exists_restrict_solution_adaptedCellAtCenter {d : ℕ} (q : Mat d) (hq : IsUnit q) (t : ℤ) (n : ℕ) {w : Fin d → ℤ} (hw : w ∈ triadicIndexBox d n) {lam Lam : ℝ} {b : Book.Ch02.CoeffOn (adaptedDomain q hq t)} {c : Book.Ch02.CoeffOn (adaptedDomainAt q hq (t - ↑n) w)} (hrep : c.toCoeffField = b.toCoeffField) (hEll : IsEllipticFieldOn lam Lam (adaptedCellAtCenter q (t - ↑n) w) c.toCoeffField) (u : Book.Ch02.Solution (adaptedDomain q hq t) b) : ∃ (z : Book.Ch02.Solution (adaptedDomainAt q hq (t - ↑n) w) c), z.toH1.grad = u.toH1.grad

The parent optimizer restricts to an admissible solution on every aligned child cell of the triadic subdivision. This is exists_restrict_solution_adaptedCellAtCenter, whose membership hypothesis hmem : adaptedCellCenter q j w ∈ adaptedCell q p is here the tree's own indexing hypothesis w ∈ triadicIndexBox d n, through adaptedCellAtCenter_subset_adaptedCell .

Canonical response-maximizer selection: comparison and carrier measurability

The pointwise Nonempty.some used by ResponseCutoffEstimate.lean is not definitionally the Chapter-2 canonical maximizer. Nevertheless, Chapter 2 uniqueness shows that their gradients, fluxes, and every subcell average of the doubled state agree almost everywhere. The second part records, on the library's actual coefficient carrier, the smooth entry-test measurability needed by the Galerkin selection construction.

noncomputable def HCPolySupport.HighContrast.Multiscale.scalarCanonicalMaximizerOfCoeffOn {d : ℕ} {U : Book.Ch02.Domain d} (a : Book.Ch02.CoeffOn U) (p q : Vec d) : ScalarCanonicalMaximizer U.carrier p q a.toCoeffField

The Chapter-2 canonical maximizer, repackaged on the scalar-response carrier of the entry route.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.HighContrast.Multiscale.canonicalAHarmonicFunctionOfCoeffOn {d : ℕ} {U : Book.Ch02.Domain d} (a : Book.Ch02.CoeffOn U) (p q : Vec d) : AHarmonicFunction a.toCoeffField U.carrier

The harmonic-function projection of the preceding canonical package.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.HighContrast.Multiscale.scalarCanonicalMaximizer_grad_ae_eq_canonicalOfCoeffOn {d : ℕ} {U : Book.Ch02.Domain d} (a : Book.Ch02.CoeffOn U) (p q : Vec d) (v : ScalarCanonicalMaximizer U.carrier p q a.toCoeffField) : (canonicalAHarmonicFunctionOfCoeffOn a p q).toH1.grad =ᵐ[volumeMeasureOn U.carrier] v.toAHarmonicFunctionMeanZero.toAHarmonicFunction.toH1.grad

STEP ZERO. An arbitrary scalar canonical maximizer (in particular the fresh Nonempty.some in ResponseCutoffEstimate.lean) has the same gradient a.e. as the specific Chapter-2 canonical family used by the measurable-selection construction.

def HCPolySupport.HighContrast.Multiscale.scalarCanonicalMaximizerOfAEEq {d : ℕ} {U : Set (Vec d)} {a b : CoeffField d} (h : a =ᵐ[volumeMeasureOn U] b) (p q : Vec d) (v : ScalarCanonicalMaximizer U p q a) : ScalarCanonicalMaximizer U p q b

Transport a specified scalar maximizer across an a.e. equality of coefficients. Unlike the existence-only bridge nonempty_scalarCanonicalMaximizer_of_aeEq (HCPoly/Entry/Response/Core/ScalarMaximizerExistence.lean), this keeps the chosen object visible for STEP ZERO.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.HighContrast.Multiscale.scalarCanonicalMaximizer_grad_ae_eq_canonicalOfAEEq {d : ℕ} {U : Book.Ch02.Domain d} {b f : CoeffField d} {lam Lam : ℝ} (hlam : 0 < lam) (hle : lam ≤ Lam) (hEll : IsEllipticFieldOn lam Lam U.carrier f) (h : b =ᵐ[volumeMeasureOn U.carrier] f) (p q : Vec d) (v : ScalarCanonicalMaximizer U.carrier p q b) : (canonicalAHarmonicFunctionOfCoeffOn (coeffOnOfIsEllipticFieldOn hlam hle hEll) p q).toH1.grad =ᵐ[volumeMeasureOn U.carrier] v.toAHarmonicFunctionMeanZero.toAHarmonicFunction.toH1.grad

STEP ZERO on the actual coefficient shape. If b only has a pointwise elliptic representative f, the arbitrary Nonempty.some maximizer for b still agrees a.e. in gradient with the Chapter-2 canonical maximizer for f, after the canonical null-set transport.

theorem HCPolySupport.HighContrast.Multiscale.optimizerField_scalarCanonicalMaximizer_ae_eq_canonicalOfAEEq {d : ℕ} {U : Book.Ch02.Domain d} {b f : CoeffField d} {lam Lam : ℝ} (hlam : 0 < lam) (hle : lam ≤ Lam) (hEll : IsEllipticFieldOn lam Lam U.carrier f) (h : b =ᵐ[volumeMeasureOn U.carrier] f) (p q : Vec d) (v : ScalarCanonicalMaximizer U.carrier p q b) : optimizerField f (canonicalAHarmonicFunctionOfCoeffOn (coeffOnOfIsEllipticFieldOn hlam hle hEll) p q) =ᵐ[volumeMeasureOn U.carrier] optimizerField b v.toAHarmonicFunctionMeanZero.toAHarmonicFunction

The comparison includes the flux: the coefficient equality and gradient uniqueness identify the complete doubled state on the parent cell.

theorem HCPolySupport.HighContrast.Multiscale.cellAverage_scalarCanonicalMaximizer_eq_canonicalOfAEEq {d : ℕ} {U : Book.Ch02.Domain d} {V : Set (Vec d)} (hVU : V ⊆ U.carrier) {b f : CoeffField d} {lam Lam : ℝ} (hlam : 0 < lam) (hle : lam ≤ Lam) (hEll : IsEllipticFieldOn lam Lam U.carrier f) (h : b =ᵐ[volumeMeasureOn U.carrier] f) (p q : Vec d) (v : ScalarCanonicalMaximizer U.carrier p q b) : cellAverage V (optimizerField f (canonicalAHarmonicFunctionOfCoeffOn (coeffOnOfIsEllipticFieldOn hlam hle hEll) p q)) = cellAverage V (optimizerField b v.toAHarmonicFunctionMeanZero.toAHarmonicFunction)

In particular every strict subcell average (n ≥ 1 as well as n = 0) of the ad hoc maximizer is determined by the measurable canonical selection.

noncomputable def HCPolySupport.HighContrast.Multiscale.selectionRegCoeffField {d : ℕ} (a : CoeffSpace d) : RegCoeffField d

The library's actual a.e.-quotient coefficient carrier, realized in CG's regular carrier.

Equations

• HCPolySupport.HighContrast.Multiscale.selectionRegCoeffField a = { toFun := ↑↑a, entry_measurable := ⋯, entry_locInt := ⋯ }

@[simp]

theorem HCPolySupport.HighContrast.Multiscale.selectionRegCoeffField_toFun {d : ℕ} (a : CoeffSpace d) : (selectionRegCoeffField a).toFun = ↑↑a

theorem HCPolySupport.HighContrast.Multiscale.measurable_entryTest_selectionRegCoeffField {d : ℕ} (i j : Fin d) {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hcpt : HasCompactSupport φ) : Measurable fun (a : CoeffSpace d) => entryTestR i j φ (selectionRegCoeffField a)

The hEntry obligation of the Galerkin selection chain is dischargeable from the actual coefficient carrier and its global smooth-test sigma algebra; it is not an additional law or RawOutput hypothesis.

The two response-coefficient transformations

The Galerkin selection API uses RegCoeffField, whereas the response argument is written on the raw carrier as a ↦ a - respg F or a ↦ aᵀ + respg F. The following carrier lifts make the algebraic generator transport explicit.

noncomputable def HCPolySupport.HighContrast.Multiscale.selectionRespCoeffMinusReg {d : ℕ} (F : BlockMat d) (a : CoeffSpace d) : RegCoeffField d

The regular-carrier lift of respCoeffMinus F.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem HCPolySupport.HighContrast.Multiscale.selectionRespCoeffMinusReg_toFun {d : ℕ} (F : BlockMat d) (a : CoeffSpace d) : (selectionRespCoeffMinusReg F a).toFun = respCoeffMinus F a

theorem HCPolySupport.HighContrast.Multiscale.measurable_entryTest_selectionRespCoeffMinusReg {d : ℕ} (F : BlockMat d) (i j : Fin d) {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hcpt : HasCompactSupport φ) : Measurable fun (a : CoeffSpace d) => entryTestR i j φ (selectionRespCoeffMinusReg F a)

Smooth compactly-supported entry tests of respCoeffMinus F are measurable on the actual coefficient carrier.

noncomputable def HCPolySupport.HighContrast.Multiscale.selectionRespCoeffPlusReg {d : ℕ} (F : BlockMat d) (a : CoeffSpace d) : RegCoeffField d

The regular-carrier lift of respCoeffPlus F.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem HCPolySupport.HighContrast.Multiscale.selectionRespCoeffPlusReg_toFun {d : ℕ} (F : BlockMat d) (a : CoeffSpace d) : (selectionRespCoeffPlusReg F a).toFun = respCoeffPlus F a

theorem HCPolySupport.HighContrast.Multiscale.measurable_entryTest_selectionRespCoeffPlusReg {d : ℕ} (F : BlockMat d) (i j : Fin d) {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hcpt : HasCompactSupport φ) : Measurable fun (a : CoeffSpace d) => entryTestR i j φ (selectionRespCoeffPlusReg F a)

Smooth compactly-supported entry tests of respCoeffPlus F are measurable on the actual coefficient carrier; transpose merely swaps the tested indices.