High-contrast homogenization:

Provider.PolynomialHomogenization.Root.Corrector.PushforwardTransport

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

The affine pushforward of a normalized-gauge corrector

The physical corrector is defined as the affine pushforward, by the normalized root, of a normalized-gauge corrector carrier. This module builds the transport that makes the physical corrector equation a consequence of the normalized one: the available physical/normalized Liouville equivalence, read in the mpr direction at the pushed-forward pair.

Nothing here selects a family; the carrier is a parameter. What is proved is that the gauge costs nothing once the construction is placed in the normalized frame.

noncomputable def HCPolySupport.HighContrast.Root.gaugeRoot {d : ℕ} (abar : Mat d) : Mat d

The normalized root attached to a homogenized matrix, as a total definition (positive definiteness is used only by the proofs).

Equations

• HCPolySupport.HighContrast.Root.gaugeRoot abar = HCPolySupport.HighContrast.Selection.normalizedRoot (HCPolySupport.symmPart abar)

noncomputable def HCPolySupport.HighContrast.Root.pushforwardValue {d : ℕ} (abar : Mat d) (G : NormalizedLocalH1Carrier d) (x : Vec d) : ℝ

The affine pushforward of a normalized-gauge corrector value.

Equations

• HCPolySupport.HighContrast.Root.pushforwardValue abar G x = G.globalValueRepresentative (HCPolySupport.matVecMul (HCPolySupport.HighContrast.Root.gaugeRoot abar)⁻¹ x)

noncomputable def HCPolySupport.HighContrast.Root.pushforwardGradient {d : ℕ} (abar : Mat d) (G : NormalizedLocalH1Carrier d) (x : Vec d) : Vec d

The affine pushforward of a normalized-gauge corrector gradient.

Equations

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

Gauge algebra

theorem HCPolySupport.HighContrast.Root.isUnit_det_gaugeRoot {d : ℕ} [NeZero d] {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) : IsUnit (Matrix.det (gaugeRoot abar))

theorem HCPolySupport.HighContrast.Root.matTranspose_gaugeRoot {d : ℕ} [NeZero d] {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) : matTranspose (gaugeRoot abar) = gaugeRoot abar

theorem HCPolySupport.HighContrast.Root.gaugeRoot_inv_apply {d : ℕ} [NeZero d] {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) (x : Vec d) : matVecMul (gaugeRoot abar)⁻¹ (matVecMul (gaugeRoot abar) x) = x

theorem HCPolySupport.HighContrast.Root.gaugeRoot_apply_inv {d : ℕ} [NeZero d] {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) (x : Vec d) : matVecMul (gaugeRoot abar) (matVecMul (gaugeRoot abar)⁻¹ x) = x

theorem HCPolySupport.HighContrast.Root.vecDot_gaugeRoot_comm {d : ℕ} [NeZero d] {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) (e y : Vec d) : vecDot e (matVecMul (gaugeRoot abar) y) = vecDot (matVecMul (gaugeRoot abar) e) y

The normalized-gauge coefficient

noncomputable def HCPolySupport.HighContrast.Root.gaugeCoeff {d : ℕ} [NeZero d] (a : CoeffSpace d) (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) : CoeffField d

The normalized-gauge coefficient field of a sample at a homogenized matrix.

Equations

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

theorem HCPolySupport.HighContrast.Root.isAELocallyUniformlyElliptic_gaugeCoeff {d : ℕ} [NeZero d] (a : CoeffSpace d) (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) : IsAELocallyUniformlyElliptic (gaugeCoeff a abar hS)

The normalized-gauge coefficient is locally uniformly elliptic, with constants read off the sample on each ball.

noncomputable def HCPolySupport.HighContrast.Root.normalizedSample {d : ℕ} [NeZero d] (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (a : CoeffSpace d) : CoeffSpace d

The normalized sample. The sample read in the normalized gauge, as an element of the coefficient space itself. This is the object the whole corrector construction can be run on: RootCorrectorEvent d (normalizedSample abar hS a) is the normalized-gauge datum, and every growth row, intrinsic slope and identification of that construction applies to it unchanged.

Equations

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

theorem HCPolySupport.HighContrast.Root.normalizedSample_ae {d : ℕ} [NeZero d] (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (a : CoeffSpace d) : ↑↑(normalizedSample abar hS a) =ᵐ[MeasureTheory.volume] gaugeCoeff a abar hS

The normalized sample is represented almost everywhere by the normalized-gauge coefficient field.

The transport

theorem HCPolySupport.HighContrast.Root.pushforward_memLiouvilleClass {d : ℕ} [NeZero d] (a : CoeffSpace d) (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (G : NormalizedLocalH1Carrier d) (e : Vec d) {theta : ℝ} (hLiou : MemLiouvilleClass (gaugeCoeff a abar hS) theta (fun (y : Vec d) => vecDot (matVecMul (gaugeRoot abar) e) y + G.globalValueRepresentative y) fun (y : Vec d) => matVecMul (gaugeRoot abar) e + G.globalGradientRepresentative y) : MemLiouvilleClass (fun (x : Vec d) => ↑↑a x) theta (fun (x : Vec d) => vecDot e x + pushforwardValue abar G x) fun (x : Vec d) => e + pushforwardGradient abar G x

The pushforward transport. A normalized-gauge Liouville-class corrector at the pulled-back slope pushes forward to a physical Liouville-class corrector at the original slope. Its weak-solution component is exactly the corrector equation clause of the stationary corrector family clause.

theorem HCPolySupport.HighContrast.Root.pushforward_isWeakSolutionOn {d : ℕ} [NeZero d] (a : CoeffSpace d) (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (G : NormalizedLocalH1Carrier d) (e : Vec d) {theta : ℝ} (hLiou : MemLiouvilleClass (gaugeCoeff a abar hS) theta (fun (y : Vec d) => vecDot (matVecMul (gaugeRoot abar) e) y + G.globalValueRepresentative y) fun (y : Vec d) => matVecMul (gaugeRoot abar) e + G.globalGradientRepresentative y) : IsWeakSolutionOn (fun (x : Vec d) => ↑↑a x) Set.univ fun (x : Vec d) => e + pushforwardGradient abar G x

The corrector equation of the pushforward family.