Documentation

LeanPool.HighContrastHomogenization.Support.Book.Ch04.CoeffFamily

Coarse-graining support: Support.Book.Ch04.CoeffFamily #

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Dependent coefficient-family bridge #

The reboot avoids the old totalized coefficient-field bridge. To build Chapter 2 objects from a Chapter 4 coefficient field, callers provide the actual AELocallyUniformlyEllipticField witness. This keeps support assumptions explicit and prevents hidden identity-totalization wrappers from leaking into Chapter 5.

source
noncomputable def HCPolySupport.Book.Ch04.coeffOnOfAEEllipticOn {d : ℕ} (a : RegCoeffField d) (Q : TriadicCube d) (hQ : ∃ (lam : ℝ) (Lam : ℝ), 0 < lam ∧ lam ≤ Lam ∧ AEEllipticOn lam Lam (openCubeSet Q) a) :
Ch02.CoeffOn (Ch02.cubeDomain Q)

The Chapter 2 coefficient object on one triadic cube obtained from a Chapter 4 a.e. ellipticity witness.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem HCPolySupport.Book.Ch04.coeffOnOfAEEllipticOn_toCoeffField {d : ℕ} (a : RegCoeffField d) (Q : TriadicCube d) (hQ : ∃ (lam : ℝ) (Lam : ℝ), 0 < lam ∧ lam ≤ Lam ∧ AEEllipticOn lam Lam (openCubeSet Q) a) :
    (coeffOnOfAEEllipticOn a Q hQ).toCoeffField = a.toFun
    source
    noncomputable def HCPolySupport.Book.Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField {d : ℕ} (a : RegCoeffField d) (h : AELocallyUniformlyEllipticField a) :
    Ch02.TriadicCoeffFamily d

    The Chapter 2 triadic coefficient family associated to a Chapter 4 a.e.-locally elliptic coefficient field.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem HCPolySupport.Book.Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField_coeffOn_toCoeffField {d : ℕ} (a : RegCoeffField d) (h : AELocallyUniformlyEllipticField a) (Q : TriadicCube d) :
      ((triadicCoeffFamilyOfAELocallyUniformlyEllipticField a h).coeffOn Q).toCoeffField = a.toFun
      source
      theorem HCPolySupport.Book.Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField_aeeq {d : ℕ} {a : RegCoeffField d} (h₁ h₂ : AELocallyUniformlyEllipticField a) :
      (triadicCoeffFamilyOfAELocallyUniformlyEllipticField a h₁).AEEq (triadicCoeffFamilyOfAELocallyUniformlyEllipticField a h₂)

      Changing only ellipticity witnesses does not change the associated triadic family modulo Chapter 2 a.e. equality.

      source
      theorem HCPolySupport.Book.Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField_aeeq_of_forall_ae_eq {d : ℕ} {a b : RegCoeffField d} (ha : AELocallyUniformlyEllipticField a) (hb : AELocallyUniformlyEllipticField b) (hab : ∀ (Q : TriadicCube d), a.toFun =ᵐ[volumeMeasureOn (openCubeSet Q)] b.toFun) :
      (triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha).AEEq (triadicCoeffFamilyOfAELocallyUniformlyEllipticField b hb)

      If two fields agree a.e. on every triadic cube, their dependent Chapter 2 triadic coefficient families agree a.e. on every cube.

      source
      theorem HCPolySupport.Book.Ch04.coeffOnOfAELocallyUniformlyEllipticField_aeeq_of_ae_eq_on_openCubeSet {d : ℕ} {a b : RegCoeffField d} (ha : AELocallyUniformlyEllipticField a) (hb : AELocallyUniformlyEllipticField b) (Q : TriadicCube d) (hab : a.toFun =ᵐ[volumeMeasureOn (openCubeSet Q)] b.toFun) :
      ((triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha).coeffOn Q).AEEq ((triadicCoeffFamilyOfAELocallyUniformlyEllipticField b hb).coeffOn Q)

      A one-cube a.e. equality of ambient fields gives a.e. equality of the corresponding Chapter 2 coefficient objects on that cube.

      source
      theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.ae_coeffFamily_exists {d : ℕ} {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) :
      ∀ᵐ (a : RegCoeffField d) ∂P, ∃ (h : AELocallyUniformlyEllipticField a) (F : Ch02.TriadicCoeffFamily d), F = triadicCoeffFamilyOfAELocallyUniformlyEllipticField a h

      A Chapter 4 law carrier supplies, almost surely, the dependent Chapter 2 triadic coefficient family associated to the sampled coefficient field.