Coarse-graining support: Support.Book.Ch01.Theorems.PotentialSolenoidal

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

theorem HCPolySupport.Book.Ch01.potentialFieldOn_of_h1 {d : ℕ} {U : Set (Vec d)} (u : H1Function U) : PotentialFieldOn U u.grad

Gradients of H¹ functions are public a.e.-based potential fields.

theorem HCPolySupport.Book.Ch01.potentialZeroTraceFieldOn_of_h10 {d : ℕ} {U : Set (Vec d)} (u : H10Function U) : PotentialZeroTraceFieldOn U u.grad

Gradients of H¹₀ functions are public a.e.-based zero-trace potential fields.

theorem HCPolySupport.Book.Ch01.PotentialZeroTraceFieldOn.potentialFieldOn {d : ℕ} {U : Set (Vec d)} {f : Vec d → Vec d} (hf : PotentialZeroTraceFieldOn U f) : PotentialFieldOn U f

Zero-trace potential fields are potential fields, at the public a.e. surface.

theorem HCPolySupport.Book.Ch01.SolenoidalZeroNormalTraceFieldOn.solenoidalFieldOn {d : ℕ} {U : Set (Vec d)} {g : Vec d → Vec d} (hg : SolenoidalZeroNormalTraceFieldOn U g) : SolenoidalFieldOn U g

Solenoidal fields with zero normal trace are solenoidal fields.