High-contrast homogenization: Entry.Response.Core.AffineSobolevPullback

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

H¹ under an invertible linear pullback

This file extends the H¹-function calculus to invertible linear pullbacks: composing an H¹ function with an invertible linear change of coordinates again yields an H¹ function, with the weak gradient transforming by the transpose of the matrix. It identifies the image of the reference cube under such a pullback with an adapted cell. For a cutoff transported by the same kind of linear change of variables, it records the chain rule for the transported gradient and the adjoint pairing identities distributing the grid between the two slots of the pulled-back pairing. These are the change-of-variables ingredients of the cutoff argument in e.response.cutoff.estimate, and the pulled-back H¹ witness on the reference cube is the input that the response transfer p.response.transfer consumes. The module also records two short facts feeding the diagonal weak-norm estimate e.response.weak.estimate: the branch-free bound on its finite-window head, and the integrability of the doubled optimizer field on a subcell.

The branch-free head bound of the cell-average estimate

The cell-average estimate e.response.weak.estimate controls its finite-window head by a tail term whose weight changes across the cutoff 1 of the all-scale maximum M: on M ≤ 1 the head is bounded through the older-scale weight 3 ^ (-(Quenched.contrastAlpha γ * H)), while on 1 < M the whole head is absorbed by the recent-scale weight √M alone. This module assembles the two branch bounds into a single estimate whose right-hand side carries the printed selector if 1 < M then √M else 3 ^ (-(Quenched.contrastAlpha γ * H)), so that a consumer carrying M need not decide which side of the cutoff it lies on.

Both branch bounds enter as hypotheses and the head, the finite sums, the tail factor and the two branch constants are abstract, so nothing here depends on how either branch is proved.

theorem HCPolySupport.HighContrast.Multiscale.head_le_add_max_mul_ite {γ : ℝ} (hγ : γ ∈ Set.Ico 0 1) (H : ℕ) {M : ℝ} (hM0 : 0 ≤ M) (Head Sums Tail cgood cbad : ℝ) (hcgood : 0 ≤ cgood) (hcbad : 0 ≤ cbad) (hSums : 0 ≤ Sums) (hTail : 0 ≤ Tail) (hgood : M ≤ 1 → Head ≤ Sums + cgood * 3 ^ (-(Quenched.contrastAlpha γ * ↑H)) * Tail) (hbad : 1 < M → Head ≤ cbad * √M * Tail) : Head ≤ Sums + (max cgood cbad * if 1 < M then √M else 3 ^ (-(Quenched.contrastAlpha γ * ↑H))) * Tail

The branch-free head bound behind e.response.weak.estimate. If the head is bounded by Sums + cgood * 3 ^ (-(Quenched.contrastAlpha γ * H)) * Tail on M ≤ 1 and by cbad * √M * Tail on 1 < M, with Sums, Tail and the two constants nonnegative, then it is bounded by Sums plus max cgood cbad times the printed selector `if 1 < M then √M else 3 ^ (-(Quenched.contrastAlpha γ

• H))times `Tail. The good-branch weight is 3 ^ (-(Quenched.contrastAlpha γ * H))rather than1, and must occur with that factor in the M ≤ 1` hypothesis for the bound to hold.

Integrability of the doubled optimizer field on a subcell

Every cell-average step of the diagonal weak-norm estimate moves a matrix through the cell average of the doubled optimizer field optimizerField b u = (∇v, b ∇v), so each such step needs both slots of that field to be integrable on the cell.

The gradient slot is L² because it is the weak gradient of an H¹ function, and L² of a finite measure is L¹. The flux slot is L² because a uniformly elliptic coefficient field is essentially bounded on the set where it is elliptic, and the product of a bounded measurable field with an L² gradient is again L².

The ellipticity hypothesis on the flux slot cannot be dropped. For instance on (0,1) take ∇v ≡ 1 (an L² gradient) and the measurable but unbounded scalar field b x = x⁻¹: then the gradient slot is L² while the flux b ∇v = x⁻¹ is not L¹. So a bound on the coefficient field is exactly what makes the flux slot integrable.

The gradient is L² only on the domain U to which the AHarmonicFunction is attached, so these statements are asked on subsets V ⊆ U. In the estimate the relevant subsets are the triadic subcells adaptedCellAtCenter q (t - n) w of HighContrast.adaptedCell q t, which is why the box version below carries the membership w ∈ triadicIndexBox d n.

theorem HCPolySupport.HighContrast.Multiscale.integrableOn_optimizerField_fst_pub {d : ℕ} {U V : Set (Vec d)} (hVU : V ⊆ U) (hVfin : MeasureTheory.volume V ≠ ⊤) (b : CoeffField d) (u : AHarmonicFunction b U) (j : Fin d) : MeasureTheory.IntegrableOn (fun (x : Vec d) => (optimizerField b u x).1 j) V MeasureTheory.volume

The gradient slot of the doubled optimizer field is integrable on every finite-measure subset of the domain: H1Function.gradMemL2 gives L², and L² ⊆ L¹ there.

The gradient of a pulled-back cutoff

The linear change of variables x = q y transports a cutoff φ from the adapted cell to the reference cube as y ↦ φ (q y). Its gradient is qᵀ applied to the gradient of φ at q y. The two declarations below record the adjoint identity for the Euclidean pairing and the chain rule in the coordinatewise gradient convention of the project. This is the linear-algebraic step of the cutoff argument in the response estimate e.response.cutoff.estimate (AK.HC Lemma A.1, (A.4)).

theorem HCPolySupport.HighContrast.Multiscale.vecDot_matVecMul_transpose {d : ℕ} (q : Mat d) (v z : Vec d) : vecDot (matVecMul (matTranspose q) v) z = vecDot v (matVecMul q z)

The adjoint identity for the Euclidean pairing: the transpose qᵀ is the adjoint of q with respect to vecDot, i.e. ⟪qᵀ v, z⟫ = ⟪v, q z⟫.

theorem HCPolySupport.HighContrast.Multiscale.fderiv_comp_matVecMul_basisVec {d : ℕ} (q : Mat d) {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (y : Vec d) : (fun (j : Fin d) => (fderiv ℝ (fun (z : Vec d) => φ (matVecMul q z)) y) (basisVec j)) = matVecMul (matTranspose q) fun (j : Fin d) => (fderiv ℝ φ (matVecMul q y)) (basisVec j)

The chain rule for the linear change of variables x = q y, in the coordinatewise gradient convention of the project: the gradient of the pulled-back function y ↦ φ (q y) is qᵀ applied to the gradient of φ at q y, i.e. (fun j => (fderiv ℝ (φ ∘ q)) y (basisVec j)) = matVecMul qᵀ (fun j => (fderiv ℝ φ (q y)) (basisVec j)).

The two slots of the pulled-back pairing

A linear change of variables x = q y transports a cutoff φ to y ↦ φ (q y). The gradient of the transported cutoff is the transpose qᵀ applied to the gradient of φ at q y; this is the chain rule recorded in fderiv_comp_matVecMul_basisVec. The three declarations below collect the linear-algebraic consequences needed to distribute the grid q between the two slots of the Euclidean pairing without cost: when one slot of the pairing is pulled back by q⁻¹, the other acquires qᵀ, and the adjointness of qᵀ cancels the two against each other. This is the change-of-variables step of the cutoff argument in the response estimate e.response.cutoff.estimate (AK.HC Lemma A.1, (A.4)).

theorem HCPolySupport.HighContrast.Multiscale.matVecMul_matVecMul_inv_cancel {d : ℕ} {q : Mat d} (hq : IsUnit q) (v : Vec d) : matVecMul q (matVecMul q⁻¹ v) = v

For an invertible matrix q, the inverse q⁻¹ cancels q under matVecMul: applying q to q⁻¹ v returns v.

theorem HCPolySupport.HighContrast.Multiscale.scalarCutoffGradientField_comp_eq {d : ℕ} (q : Mat d) {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (y : Vec d) : scalarCutoffGradientField (fun (z : Vec d) => φ (matVecMul q z)) y = matVecMul (matTranspose q) (scalarCutoffGradientField φ (matVecMul q y))

The gradient of the pulled-back cutoff y ↦ φ (q y) is qᵀ applied to the gradient of φ at q y, in the coordinatewise gradient convention of the project: the gradient field of the composition is the transpose of the grid applied to the pulled-back gradient field.

theorem HCPolySupport.HighContrast.Multiscale.vecDot_pullback_slots {d : ℕ} {q : Mat d} (hq : IsUnit q) {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (v y : Vec d) : vecDot (matVecMul q⁻¹ v) (scalarCutoffGradientField (fun (z : Vec d) => φ (matVecMul q z)) y) = vecDot v (scalarCutoffGradientField φ (matVecMul q y))

The Euclidean pairing is preserved when the first slot acquires q⁻¹ and the second the transpose of the grid: for an invertible q, ⟪q⁻¹ v, ∇(φ ∘ q)(y)⟫ = ⟪v, ∇φ(q y)⟫.

H¹ under an invertible linear pullback

The pinned CoarseGraining revision 8ec687c has H1Function constructors for restriction (Sobolev/H1/BasicLemmas.lean), domain casts (Book/Ch03/Theorems/PublicInternalBridges/H1Casts.lean), translation (Sobolev/H1/Translation.lean), positive scalar dilation (Sobolev/Foundations/CoerciveH1Dilation.lean) and the two measure-preserving symmetries of the centred cube — coordinate sign flip and coordinate swap (Sobolev/H1/OriginCubeSymmetry.lean) — but no pullback along a general invertible linear map. That is what this file adds.

The construction is u ↦ u ∘ q with the chain-rule gradient qᵀ (∇u ∘ q). Unlike the sign-flip and swap cases, y ↦ q y is not measure preserving, so the L² and weak-derivative transfers both carry the Jacobian factor |det q|⁻¹; it cancels between the two sides of the weak formulation, which is why no hypothesis on det q beyond invertibility is needed.

Everything is stated for a general source set V with q V ⊆ U. For p.response.transfer, the instance q = respGrid jStar F, V = openCubeSet (originCube d t), U = adaptedCell q t is proved inhabited in the last section.

The linear change of variables x = q y

noncomputable def HCPolySupport.HighContrast.Multiscale.matHomeomorph {d : ℕ} {q : Mat d} (hq : IsUnit q) : Vec d ≃ₜ Vec d

An invertible matrix acts on Vec d as a homeomorphism.

Equations

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

@[simp]

theorem HCPolySupport.HighContrast.Multiscale.matHomeomorph_apply {d : ℕ} {q : Mat d} (hq : IsUnit q) (x : Vec d) : (matHomeomorph hq) x = matVecMul q x

@[simp]

theorem HCPolySupport.HighContrast.Multiscale.matHomeomorph_symm_apply {d : ℕ} {q : Mat d} (hq : IsUnit q) (x : Vec d) : (matHomeomorph hq).symm x = matVecMul q⁻¹ x

theorem HCPolySupport.HighContrast.Multiscale.matVecMul_inv_matVecMul {d : ℕ} {q : Mat d} (hq : IsUnit q) (x : Vec d) : matVecMul q⁻¹ (matVecMul q x) = x

theorem HCPolySupport.HighContrast.Multiscale.isOpen_image_matVecMul {d : ℕ} {q : Mat d} (hq : IsUnit q) {V : Set (Vec d)} (hV : IsOpen V) : IsOpen (matVecMul q '' V)

theorem HCPolySupport.HighContrast.Multiscale.measurableEmbedding_matVecMul {d : ℕ} {q : Mat d} (hq : IsUnit q) : MeasurableEmbedding (matVecMul q)

theorem HCPolySupport.HighContrast.Multiscale.map_matVecMul_volume_restrict {d : ℕ} {q : Mat d} (hq : IsUnit q) (V : Set (Vec d)) : MeasureTheory.Measure.map (matVecMul q) (MeasureTheory.volume.restrict V) = ENNReal.ofReal |Matrix.det q|⁻¹ • MeasureTheory.volume.restrict (matVecMul q '' V)

The push-forward of restricted Lebesgue measure under an invertible linear map: the Jacobian factor |det q|⁻¹ times restricted Lebesgue measure on the image.

theorem HCPolySupport.HighContrast.Multiscale.setIntegral_comp_matVecMul_image {d : ℕ} {q : Mat d} (hq : IsUnit q) (V : Set (Vec d)) (g : Vec d → ℝ) : ∫ (y : Vec d) in V, g (matVecMul q y) = |Matrix.det q|⁻¹ * ∫ (x : Vec d) in matVecMul q '' V, g x

The set-integral change of variables x = q y, with no integrability hypothesis (both sides are Bochner junk values together).

L² under the pullback

theorem HCPolySupport.HighContrast.Multiscale.memL2On_comp_matVecMul {d : ℕ} {q : Mat d} (hq : IsUnit q) {U V : Set (Vec d)} (hsub : matVecMul q '' V ⊆ U) {f : Vec d → ℝ} (hf : MemL2On U f) : MemL2On V fun (y : Vec d) => f (matVecMul q y)

L² transfers along the pullback: the Jacobian factor is a finite positive constant, so it changes nothing about membership.

theorem HCPolySupport.HighContrast.Multiscale.gradMemL2On_matVecMul_comp_matVecMul {d : ℕ} {q : Mat d} (hq : IsUnit q) (A : Mat d) {U V : Set (Vec d)} (hsub : matVecMul q '' V ⊆ U) {G : Vec d → Vec d} (hG : GradMemL2On U G) : GradMemL2On V fun (y : Vec d) => matVecMul A (G (matVecMul q y))

A coordinatewise-L² vector field on U pulls back to one on V, after any fixed linear post-composition A. With A = qᵀ this is the gradient slot of the H¹ pullback; with A = q⁻¹ it is the flux slot of the p.response.transfer pairing.

The chain rule for x = q y

theorem HCPolySupport.HighContrast.Multiscale.matVecMul_basisVec {d : ℕ} (q : Mat d) (i : Fin d) : matVecMul q (basisVec i) = ∑ j : Fin d, q j i • basisVec j

The image of a coordinate basis vector is the matching column.

theorem HCPolySupport.HighContrast.Multiscale.matVecMul_matTranspose_apply {d : ℕ} (q : Mat d) (w : Vec d) (i : Fin d) : matVecMul (matTranspose q) w i = ∑ j : Fin d, q j i * w j

The i-th coordinate of qᵀ w.

theorem HCPolySupport.HighContrast.Multiscale.fderiv_apply_basisVec_comp_matVecMul_inv {d : ℕ} {q : Mat d} (hq : IsUnit q) {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (i : Fin d) (x : Vec d) : (fderiv ℝ φ (matVecMul q⁻¹ x)) (basisVec i) = ∑ j : Fin d, q j i * (fderiv ℝ (fun (z : Vec d) => φ (matVecMul q⁻¹ z)) x) (basisVec j)

The chain rule in the shape the weak formulation consumes: the i-th partial of φ at q⁻¹ x is the q-weighted combination of the partials of φ ∘ q⁻¹ at x.

The weak gradient under the pullback

theorem HCPolySupport.HighContrast.Multiscale.hasWeakGradientOn_comp_matVecMul {d : ℕ} {q : Mat d} (hq : IsUnit q) {V : Set (Vec d)} {u : Vec d → ℝ} {Du : Vec d → Vec d} (hu : MemL2On (matVecMul q '' V) u) (hDu : GradMemL2On (matVecMul q '' V) Du) (h : HasWeakGradientOn (matVecMul q '' V) u Du) : HasWeakGradientOn V (fun (y : Vec d) => u (matVecMul q y)) fun (y : Vec d) => matVecMul (matTranspose q) (Du (matVecMul q y))

The weak-gradient pullback. If u has weak gradient Du on the image q V, then u ∘ q has weak gradient qᵀ (Du ∘ q) on V. The L² hypotheses are used only to move the finite sum of the chain rule through the integral.

The H¹ constructor

def HCPolySupport.HighContrast.Multiscale.pullbackMatVecMul {d : ℕ} {q : Mat d} (hq : IsUnit q) {U V : Set (Vec d)} (hV : IsOpen V) (hsub : matVecMul q '' V ⊆ U) (u : H1Function U) : H1Function V

The H¹-under-linear-pullback constructor. For an invertible q and an open V whose image q V lies in the domain U, the pullback y ↦ u (q y) is an H¹(V) witness with the chain-rule gradient y ↦ qᵀ (∇u (q y)).

The hypotheses are exactly: invertibility of q, openness of the source set, and the image containment. No hypothesis is placed on det q beyond invertibility, and none on U.

Equations

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

@[simp]

theorem HCPolySupport.HighContrast.Multiscale.pullbackMatVecMul_toFun {d : ℕ} {q : Mat d} (hq : IsUnit q) {U V : Set (Vec d)} (hV : IsOpen V) (hsub : matVecMul q '' V ⊆ U) (u : H1Function U) : (pullbackMatVecMul hq hV hsub u).toFun = fun (y : Vec d) => u.toFun (matVecMul q y)

@[simp]

theorem HCPolySupport.HighContrast.Multiscale.pullbackMatVecMul_grad {d : ℕ} {q : Mat d} (hq : IsUnit q) {U V : Set (Vec d)} (hV : IsOpen V) (hsub : matVecMul q '' V ⊆ U) (u : H1Function U) : (pullbackMatVecMul hq hV hsub u).grad = fun (y : Vec d) => matVecMul (matTranspose q) (u.grad (matVecMul q y))

Satisfiability of the hypothesis bundle at q = respGrid jStar F

The constructor above would be worthless if its hypothesis bundle were empty in the situation p.response.transfer needs. It is not: at q = respGrid jStar F the bundle is inhabited, and the image containment even holds with EQUALITY, because adaptedCell q t is by definition q applied to the centred cube centeredCube d t = openCubeSet (originCube d t).

Invertibility, however, is NOT available from (explicitCanonicalMetric F).PosDef alone: the only route to IsUnit (explicitRoundedGrid jStar m) in the tree is Geometry.isUnit_roundedGrid (HCPoly/Entry/Geometry/RoundedGridBasic.lean), which also consumes 2 * d ≤ 3 ^ jStar — the same premise that explicitRoundedGrid_metricFrobenius_product_le (ScaleAverageSeminorm.lean) carries. It is therefore carried here as a hypothesis, not silently assumed.

theorem HCPolySupport.HighContrast.Multiscale.isUnit_respGrid {d jStar : ℕ} (hjStar : 2 * d ≤ 3 ^ jStar) {F : BlockMat d} (hm : Matrix.PosDef (explicitCanonicalMetric F)) : IsUnit (respGrid jStar F)

The selected grid is invertible on the PosDef branch, provided the grid depth satisfies 2 * d ≤ 3 ^ jStar.

theorem HCPolySupport.HighContrast.Multiscale.image_openCubeSet_originCube_eq_adaptedCell {d : ℕ} (q : Mat d) (t : ℤ) : matVecMul q '' openCubeSet (originCube d t) = adaptedCell q t

The adapted cell IS the q-image of the reference cube: the image containment of the constructor holds with equality at every q and every scale.

noncomputable def HCPolySupport.HighContrast.Multiscale.respPullbackH1 {d jStar : ℕ} (hjStar : 2 * d ≤ 3 ^ jStar) {F : BlockMat d} (hm : Matrix.PosDef (explicitCanonicalMetric F)) (t : ℤ) (u : H1Function (adaptedCell (respGrid jStar F) t)) : H1Function (openCubeSet (originCube d t))

Satisfiability witness. The hypothesis bundle of pullbackMatVecMul is inhabited at q = respGrid jStar F: any H¹ witness on the adapted cell U_t pulls back to an H¹ witness on the reference cube openCubeSet (originCube d t) with the chain-rule gradient.

Equations

• HCPolySupport.HighContrast.Multiscale.respPullbackH1 hjStar hm t u = HCPolySupport.HighContrast.Multiscale.pullbackMatVecMul ⋯ ⋯ ⋯ u

@[simp]

theorem HCPolySupport.HighContrast.Multiscale.respPullbackH1_toFun {d jStar : ℕ} (hjStar : 2 * d ≤ 3 ^ jStar) {F : BlockMat d} (hm : Matrix.PosDef (explicitCanonicalMetric F)) (t : ℤ) (u : H1Function (adaptedCell (respGrid jStar F) t)) : (respPullbackH1 hjStar hm t u).toFun = fun (y : Vec d) => u.toFun (matVecMul (respGrid jStar F) y)

@[simp]

theorem HCPolySupport.HighContrast.Multiscale.respPullbackH1_grad {d jStar : ℕ} (hjStar : 2 * d ≤ 3 ^ jStar) {F : BlockMat d} (hm : Matrix.PosDef (explicitCanonicalMetric F)) (t : ℤ) (u : H1Function (adaptedCell (respGrid jStar F) t)) : (respPullbackH1 hjStar hm t u).grad = fun (y : Vec d) => matVecMul (matTranspose (respGrid jStar F)) (u.grad (matVecMul (respGrid jStar F) y))

affineH1, reconstructed locally

Only declaration needed from HCPolySupport.HighContrast.Coupled.WeakForm: affineH1/affineH1_grad/affineH1_toFun (WeakForm.lean). Built there from the primitives H1Function.coordOnOpenCubeSetOriginCube (Sobolev/H1/OriginCubeBridge.lean) and add_grad/add_toFun/smul_grad/smul_toFun (Sobolev/H1/Algebra/H1Function.lean). Reproduced verbatim from those.

theorem HCPolySupport.HighContrast.Multiscale.H1Function.sum_grad {d : ℕ} {ι : Type u_1} {U : Set (Vec d)} (s : Finset ι) (f : ι → H1Function U) : (∑ i ∈ s, f i).grad = fun (x : Vec d) => ∑ i ∈ s, (f i).grad x

theorem HCPolySupport.HighContrast.Multiscale.H1Function.sum_toFun {d : ℕ} {ι : Type u_1} {U : Set (Vec d)} (s : Finset ι) (f : ι → H1Function U) : (∑ i ∈ s, f i).toFun = fun (x : Vec d) => ∑ i ∈ s, (f i).toFun x

noncomputable def HCPolySupport.HighContrast.Multiscale.affineH1 {d : ℕ} (m : ℤ) (p : Vec d) : H1Function (openCubeSet (originCube d m))

The affine map x ↦ p·x as an H¹ function on the centered open cube, with constant gradient p.

Equations

• HCPolySupport.HighContrast.Multiscale.affineH1 m p = ∑ i : Fin d, p i • HCPolySupport.H1Function.coordOnOpenCubeSetOriginCube i

@[simp]

theorem HCPolySupport.HighContrast.Multiscale.affineH1_grad {d : ℕ} (m : ℤ) (p : Vec d) : (affineH1 m p).grad = fun (x : Vec d) => p

@[simp]

theorem HCPolySupport.HighContrast.Multiscale.affineH1_toFun {d : ℕ} (m : ℤ) (p : Vec d) : (affineH1 m p).toFun = fun (x : Vec d) => vecDot p x

noncomputable def HCPolySupport.HighContrast.Multiscale.respCenteredPullbackH1 {d jStar : ℕ} (hjStar : 2 * d ≤ 3 ^ jStar) {F : BlockMat d} (hm : Matrix.PosDef (explicitCanonicalMetric F)) (t : ℤ) (b : CoeffField d) (u : AHarmonicFunction b (adaptedCell (respGrid jStar F) t)) (Y : BlockVec d) : H1Function (openCubeSet (originCube d t))

The cutoff bridge's input. The centred pulled-back potential y ↦ v(qy) − ⟨P, qy⟩ on the reference cube, as an H¹ witness whose gradient is the FIRST SLOT of the pulled-back centred optimizer field, i.e. y ↦ qᵀ ((optimizerField b u (q y) − Y).1) with P = Y.1. This is exactly the u : H1Function (openCubeSet Q) argument of the generic CG bridge abs_cubeAverage_vecDot_centered_scalar_cutoff_le_scaledWeakNormProduct (Book/Ch05/.../JUpperBoundWeakNorms/Product/Bridge.lean).

Equations

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

@[simp]

theorem HCPolySupport.HighContrast.Multiscale.respCenteredPullbackH1_toFun {d jStar : ℕ} (hjStar : 2 * d ≤ 3 ^ jStar) {F : BlockMat d} (hm : Matrix.PosDef (explicitCanonicalMetric F)) (t : ℤ) (b : CoeffField d) (u : AHarmonicFunction b (adaptedCell (respGrid jStar F) t)) (Y : BlockVec d) : (respCenteredPullbackH1 hjStar hm t b u Y).toFun = fun (y : Vec d) => u.toH1.toFun (matVecMul (respGrid jStar F) y) - vecDot Y.1 (matVecMul (respGrid jStar F) y)

@[simp]

theorem HCPolySupport.HighContrast.Multiscale.respCenteredPullbackH1_grad {d jStar : ℕ} (hjStar : 2 * d ≤ 3 ^ jStar) {F : BlockMat d} (hm : Matrix.PosDef (explicitCanonicalMetric F)) (t : ℤ) (b : CoeffField d) (u : AHarmonicFunction b (adaptedCell (respGrid jStar F) t)) (Y : BlockVec d) : (respCenteredPullbackH1 hjStar hm t b u Y).grad = fun (y : Vec d) => matVecMul (matTranspose (respGrid jStar F)) (optimizerField b u (matVecMul (respGrid jStar F) y) - Y).1