High-contrast homogenization:

Provider.PolynomialHomogenization.Root.Corrector.PushforwardGaugeAlgebra

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

Gauge algebra for the pushforward

Three elaboration hazards are avoided here deliberately; each of them costs a runaway when it is not.

• Every rewrite runs with the value and gradient fields as bare function variables. rw [matVecMul_add] has to decide, for each subterm matVecMul L⁻¹ (Ψ …), whether Ψ … is an addition; when Ψ is NormalizedLocalH1Carrier.globalGradientRepresentative G that decision delta-unfolds the carrier and, through it, the spectral selector inside gaugeRoot. With Ψ a local function variable it fails on the head symbol at once.
• Almost-everywhere statements are moved with EventuallyEq.comp_tendsto and EventuallyEq.fun_comp, never by filter_upwards on a goal whose sides are partially applied pushforwardGradient, and never by ascribing a type to the raw QuasiMeasurePreserving.tendsto_ae application.
• The algebra lemmas are applied with every argument explicit, so no higher-order unification is attempted.

theorem HCPolySupport.HighContrast.Root.pushforwardGradient_translate_ae {d : ℕ} [NeZero d] {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) {G H : NormalizedLocalH1Carrier d} (w : Vec d) (h : (fun (y : Vec d) => G.globalGradientRepresentative (y + matVecMul (gaugeRoot abar)⁻¹ w)) =ᵐ[MeasureTheory.volume] H.globalGradientRepresentative) : pushforwardGradient abar H =ᵐ[MeasureTheory.volume] fun (x : Vec d) => pushforwardGradient abar G (x + w)

The pushforward of a carrier whose gradient representative is a translate is the translate of the pushforward, with the translation vector pushed forward.

theorem HCPolySupport.HighContrast.Root.pushforwardGradient_linear_ae {d : ℕ} [NeZero d] {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) (c : ℝ) {G G1 G2 : NormalizedLocalH1Carrier d} (h : G.globalGradientRepresentative =ᵐ[MeasureTheory.volume] fun (y : Vec d) => c • G1.globalGradientRepresentative y + G2.globalGradientRepresentative y) : pushforwardGradient abar G =ᵐ[MeasureTheory.volume] fun (x : Vec d) => c • pushforwardGradient abar G1 x + pushforwardGradient abar G2 x

The pushforward is linear in the carrier, almost everywhere.