High-contrast homogenization: Provider.Response.ResponseCongruence

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

The response sees only the almost everywhere class of the coefficient

Membership in the admissible class of a variational response problem is stable under changing the coefficient on a null set: being a potential is a condition on the field alone, and being solenoidal against every compactly supported test gradient is an integral condition. The response integrand is a pointwise expression in the coefficient and the admissible gradient, so its normalized average is unchanged as well. Consequently the whole value set of the response functional, and with it the response itself, depends on the coefficient only through its almost everywhere class.

This is what turns the pathwise translation covariance of the response into a statement about a coefficient sample: the translated sample and the translated field agree almost everywhere, not everywhere. Combining the two gives the covariance under integer translations, and under a translation invariant law the annealed response of a cube depends on the cube only through its scale.

Almost everywhere stability of the admissible class

def HCPolySupport.HighContrast.Response.aHarmonicOfAEEq {d : ℕ} {U : Set (Vec d)} {f g : CoeffField d} (h : f =ᵐ[volumeMeasureOn U] g) (u : AHarmonicFunction f U) : AHarmonicFunction g U

An a-harmonic function is b-harmonic whenever a and b agree almost everywhere, with the same underlying Sobolev function.

Equations

• HCPolySupport.HighContrast.Response.aHarmonicOfAEEq h u = { toH1 := u.toH1, isHarmonic := ⋯ }

@[simp]

theorem HCPolySupport.HighContrast.Response.aHarmonicOfAEEq_grad {d : ℕ} {U : Set (Vec d)} {f g : CoeffField d} (h : f =ᵐ[volumeMeasureOn U] g) (u : AHarmonicFunction f U) : (aHarmonicOfAEEq h u).toH1.grad = u.toH1.grad

The transported admissible function has the same gradient.

Almost everywhere congruence of the response

theorem HCPolySupport.HighContrast.Response.responseJValueSet_subset_of_ae_eq {d : ℕ} (U : Set (Vec d)) (p q : Vec d) {f g : CoeffField d} (h : f =ᵐ[volumeMeasureOn U] g) : responseJValueSet U p q f ⊆ responseJValueSet U p q g

One inclusion of the value-set congruence.

theorem HCPolySupport.HighContrast.Response.responseJValueSet_congr_of_ae_eq {d : ℕ} (U : Set (Vec d)) (p q : Vec d) {f g : CoeffField d} (h : f =ᵐ[volumeMeasureOn U] g) : responseJValueSet U p q f = responseJValueSet U p q g

The response value set sees only the almost everywhere class of the coefficient.

theorem HCPolySupport.HighContrast.Response.ResponseJ_congr_of_ae_eq_restrict {d : ℕ} (U : Set (Vec d)) (p q : Vec d) {f g : CoeffField d} (h : f =ᵐ[volumeMeasureOn U] g) : ResponseJ U p q f = ResponseJ U p q g

The response sees only the almost everywhere class of the coefficient, in the form restricted to the domain.

theorem HCPolySupport.HighContrast.Response.ResponseJ_congr_of_ae_eq {d : ℕ} (U : Set (Vec d)) (p q : Vec d) {f g : CoeffField d} (h : f =ᵐ[MeasureTheory.volume] g) : ResponseJ U p q f = ResponseJ U p q g

The response sees only the almost everywhere class of the coefficient.

Covariance of the response of a sample under integer translations

theorem HCPolySupport.HighContrast.Response.ResponseJ_translateSet_intTranslation {d : ℕ} (z : Fin d → ℤ) (U : Set (Vec d)) (p q : Vec d) (a : CoeffSpace d) : ResponseJ (translateSet (Source.AKL.intTranslation z) U) p q ↑↑a = ResponseJ U p q ↑↑(translateCoeff z a)

J(U + z; a) = J(U; T_z a). The pathwise translation covariance of the response at every sample of the coefficient space.

Triadic cubes of nonnegative scale are integer translates

theorem HCPolySupport.HighContrast.Response.exists_intVec_openCubeSet_eq_translateSet {d : ℕ} (R : TriadicCube d) (hscale : 0 ≤ R.scale) : ∃ (z : Fin d → ℤ), openCubeSet R = translateSet (Source.AKL.intTranslation z) (openCubeSet (originCube d R.scale))

A triadic cube of nonnegative scale is an integer translate of the centered cube of the same scale.

theorem HCPolySupport.HighContrast.Response.exists_translateCoeff_ResponseJ_openCubeSet {d : ℕ} (R : TriadicCube d) (hscale : 0 ≤ R.scale) (p q : Vec d) : ∃ (z : Fin d → ℤ), ∀ (a : CoeffSpace d), ResponseJ (openCubeSet R) p q ↑↑a = ResponseJ (openCubeSet (originCube d R.scale)) p q ↑↑(translateCoeff z a)

The response on a triadic cube of nonnegative scale is the response on the centered cube of the same scale, at a translated sample.

The unconditional annealed vanishing

theorem HCPolySupport.HighContrast.Response.integral_descendantsAverage_cutoffWeighted_ResponseJ_eq_zero {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} (hP : IsStationaryLaw P) (Q : TriadicCube d) (j : ℕ) (hscale : 0 ≤ Q.scale - ↑j) (p q : Vec d) {φ : Vec d → ℝ} (hint : ∀ R ∈ descendantsAtDepth Q j, MeasureTheory.Integrable (fun (a : CoeffSpace d) => ResponseJ (openCubeSet R) p q ↑↑a) P) (hbase : MeasureTheory.Integrable (fun (a : CoeffSpace d) => ResponseJ (openCubeSet (originCube d (Q.scale - ↑j))) p q ↑↑a) P) (hφ : MeasureTheory.IntegrableOn φ (cubeSet Q) MeasureTheory.volume) (hmean : cubeAverage Q φ = 1) : ∫ (a : CoeffSpace d), descendantsAverage Q j fun (R : TriadicCube d) => (1 - cubeAverage R φ) * ResponseJ (openCubeSet R) p q ↑↑a ∂P = 0

The cutoff-weighted child responses vanish in the mean, with no carried covariance hypothesis. The only inputs are the stationarity of the law, the nonnegativity of the child scale, the mean-one normalization of the cutoff, and integrability.