Documentation

LeanPool.HighContrastHomogenization.Support.Book.Ch03.Theorems.PublicInternalBridges.H1Casts

Coarse-graining support: Support.Book.Ch03.Theorems.PublicInternalBridges.H1Casts #

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

Public H1 domain casts for Chapter 3 #

This file contains small domain-cast helpers used to transport public open-cube H1, H10, and mean-zero H1 data to the deterministic cube realization.

source
noncomputable def HCPolySupport.Book.Ch03.castH1Domain {d : ℕ} {U V : Set (Vec d)} (hUV : U = V) (u : H1Function U) :
H1Function V

Transport an H¹ function along an equality of its domains.

Equations
Instances For
    source
    noncomputable def HCPolySupport.Book.Ch03.castH10Domain {d : ℕ} {U V : Set (Vec d)} (hUV : U = V) (u : H10Function U) :
    H10Function V

    Transport a zero-trace H¹ function along an equality of its domains.

    Equations
    Instances For
      source
      @[simp]
      theorem HCPolySupport.Book.Ch03.castH1Domain_grad {d : ℕ} {U V : Set (Vec d)} (hUV : U = V) (u : H1Function U) :
      (castH1Domain hUV u).grad = u.grad
      source
      @[simp]
      theorem HCPolySupport.Book.Ch03.castH1Domain_toFun {d : ℕ} {U V : Set (Vec d)} (hUV : U = V) (u : H1Function U) :
      (castH1Domain hUV u).toFun = u.toFun
      source
      @[simp]
      theorem HCPolySupport.Book.Ch03.castH10Domain_toH1Function_grad {d : ℕ} {U V : Set (Vec d)} (hUV : U = V) (u : H10Function U) :
      (castH10Domain hUV u).grad = u.grad
      source
      @[simp]
      theorem HCPolySupport.Book.Ch03.castH10Domain_toH1Function_toFun {d : ℕ} {U V : Set (Vec d)} (hUV : U = V) (u : H10Function U) :
      (castH10Domain hUV u).toFun = u.toFun
      source
      noncomputable def HCPolySupport.Book.Ch03.castH1MeanZeroDomain {d : ℕ} {U V : Set (Vec d)} (hUV : U = V) (u : H1MeanZeroFunction U) :
      H1MeanZeroFunction V

      Transport a mean-zero H¹ function along an equality of its domains.

      Equations
      Instances For
        source
        @[simp]
        theorem HCPolySupport.Book.Ch03.castH1MeanZeroDomain_toH1Function_grad {d : ℕ} {U V : Set (Vec d)} (hUV : U = V) (u : H1MeanZeroFunction U) :
        (castH1MeanZeroDomain hUV u).toH1Function.grad = u.toH1Function.grad
        source
        @[simp]
        theorem HCPolySupport.Book.Ch03.castH1MeanZeroDomain_toH1Function_toFun {d : ℕ} {U V : Set (Vec d)} (hUV : U = V) (u : H1MeanZeroFunction U) :
        (castH1MeanZeroDomain hUV u).toH1Function.toFun = u.toH1Function.toFun