High-contrast homogenization: Provider.Quenched.TriadicDilationCoeff

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

Triadic dilation on the coefficient space

The coefficient-space dilation reads a sample at the points 3^n x. It is defined directly on the almost-everywhere quotient, preserves the field's own ellipticity constants, and is measurable for the sigma-field generated by smooth compactly supported linear statistics.

theorem HCPolySupport.HighContrast.CoeffSpace.quasiMeasurePreserving_const_smul {d : ℕ} (r : ℝ) (hr : r ≠ 0) : MeasureTheory.QuasiMeasurePreserving (fun (x : Vec d) => r • x) MeasureTheory.volume MeasureTheory.volume

noncomputable def HCPolySupport.HighContrast.CoeffSpace.scalarPullback {d : ℕ} (r : ℝ) (hr : r ≠ 0) (a : CoeffSpace d) : CoeffSpace d

Pullback of a locally elliptic coefficient class by the nonzero dilation x ↦ r • x.

Equations

• HCPolySupport.HighContrast.CoeffSpace.scalarPullback r hr a = ⟨MeasureTheory.AEEqFun.compQuasiMeasurePreserving (↑a) (fun (x : HCPolySupport.Vec d) => r • x) ⋯, ⋯⟩

noncomputable def HCPolySupport.HighContrast.CoeffSpace.triadicDilation {d : ℕ} (n : ℕ) (a : CoeffSpace d) : CoeffSpace d

Pull a coefficient sample back by the triadic dilation x ↦ 3^n x.

Equations

• HCPolySupport.HighContrast.CoeffSpace.triadicDilation n a = HCPolySupport.HighContrast.CoeffSpace.scalarPullback (3 ^ n) ⋯ a

noncomputable def HCPolySupport.HighContrast.CoeffSpace.triadicContraction {d : ℕ} (n : ℕ) (a : CoeffSpace d) : CoeffSpace d

The inverse carrier map to triadicDilation n.

Equations

• HCPolySupport.HighContrast.CoeffSpace.triadicContraction n a = HCPolySupport.HighContrast.CoeffSpace.scalarPullback (3 ^ n)⁻¹ ⋯ a

theorem HCPolySupport.HighContrast.CoeffSpace.triadicDilation_ae {d : ℕ} (n : ℕ) (a : CoeffSpace d) : ↑↑(triadicDilation n a) =ᵐ[MeasureTheory.volume] fun (x : Vec d) => ↑↑a (triadicDilateVec n x)

The quotient dilation has the expected representative almost everywhere.

theorem HCPolySupport.HighContrast.CoeffSpace.triadicContraction_ae {d : ℕ} (n : ℕ) (a : CoeffSpace d) : ↑↑(triadicContraction n a) =ᵐ[MeasureTheory.volume] fun (x : Vec d) => ↑↑a ((3 ^ n)⁻¹ • x)

The inverse quotient dilation reads the sample at 3⁻ⁿ x.

@[simp]

theorem HCPolySupport.HighContrast.CoeffSpace.triadicContraction_triadicDilation {d : ℕ} (n : ℕ) (a : CoeffSpace d) : triadicContraction n (triadicDilation n a) = a

Contracting a dilated quotient sample recovers the sample.

@[simp]

theorem HCPolySupport.HighContrast.CoeffSpace.triadicDilation_triadicContraction {d : ℕ} (n : ℕ) (a : CoeffSpace d) : triadicDilation n (triadicContraction n a) = a

Dilating a contracted quotient sample recovers the sample.

theorem HCPolySupport.HighContrast.CoeffSpace.coeffPairing_triadicDilation {d : ℕ} (n : ℕ) (e e' : Vec d) (phi : Vec d → ℝ) (a : CoeffSpace d) : coeffPairing e e' phi (triadicDilation n a) = ((3 ^ n) ^ d)⁻¹ * coeffPairing e e' (fun (y : Vec d) => phi ((3 ^ n)⁻¹ • y)) a

Triadic dilation pulls a generating pairing back to the inverse-dilated test, with the Jacobian factor made explicit.

theorem HCPolySupport.HighContrast.CoeffSpace.measurable_triadicDilation_coeffSigma {d : ℕ} (n : ℕ) (U : Set (Vec d)) : Measurable (triadicDilation n)

Pullback by triadic dilation is measurable from the local sigma-field on the dilated region to the local sigma-field on the original region.

theorem HCPolySupport.HighContrast.CoeffSpace.measurable_triadicDilation {d : ℕ} (n : ℕ) : Measurable (triadicDilation n)

Triadic dilation is measurable for the canonical coefficient sigma-field.

theorem HCPolySupport.HighContrast.CoeffSpace.measurable_triadicContraction {d : ℕ} (n : ℕ) : Measurable (triadicContraction n)

The inverse triadic carrier map is measurable.

noncomputable def HCPolySupport.HighContrast.CoeffSpace.triadicDilationMeasurableEquiv {d : ℕ} (n : ℕ) : CoeffSpace d ≃ᵐ CoeffSpace d

Triadic dilation is a measurable equivalence of the coefficient space.

Equations

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

theorem HCPolySupport.HighContrast.CoeffSpace.translateCoeff_triadicDilation {d : ℕ} (n : ℕ) (z : Fin d → ℤ) (a : CoeffSpace d) : translateCoeff z (triadicDilation n a) = triadicDilation n (translateCoeff (triadicScaleIntShift n z) a)

Integer translation after dilation is the dilation of the correspondingly rescaled integer translation.