Coarse-graining support: Support.Sobolev.PotentialSolenoidalExact

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

Exact potential and solenoidal spaces

This module implements the literal Hilbert-space constructions underlying the Chapter 1 potential/solenoidal quartet. The raw submodules are mathematically well-defined for an arbitrary set U, so this reusable construction is kept generic here. It is not the manuscript-facing API: Book.Ch01.FieldSpaces exposes the quartet only with IsOpenBoundedConvexDomain U and U.Nonempty. Any consequence needing those domain hypotheses states them explicitly below.

The two potential spaces are literal ranges of the typed Hilbert L² gradient maps. They are deliberately not closed: closedness is a separate analytic theorem, not part of these definitions.

noncomputable def HCPolySupport.PotentialSolenoidalExact.potential {d : ℕ} (U : Set (Vec d)) : Submodule ℝ ↥(HilbertVectorL2 U)

The generic literal range of H¹(U) gradients in the Euclidean Hilbert-vector L²(U) ambient space. The nonempty bounded open convex Chapter 1 facade is Book.Ch01.PotentialHilbertL2.

Equations

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

noncomputable def HCPolySupport.PotentialSolenoidalExact.potentialZeroTrace {d : ℕ} (U : Set (Vec d)) : Submodule ℝ ↥(HilbertVectorL2 U)

The generic literal range of H¹₀(U) gradients in the Euclidean Hilbert-vector L²(U) ambient space. The nonempty bounded open convex Chapter 1 facade is Book.Ch01.PotentialZeroTraceHilbertL2.

Equations

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

noncomputable def HCPolySupport.PotentialSolenoidalExact.solenoidal {d : ℕ} (U : Set (Vec d)) : Submodule ℝ ↥(HilbertVectorL2 U)

The generic orthogonal complement of all zero-trace potential fields. The Chapter 1 source-facing facade is Book.Ch01.SolenoidalHilbertL2.

Equations

• HCPolySupport.PotentialSolenoidalExact.solenoidal U = (HCPolySupport.PotentialSolenoidalExact.potentialZeroTrace U)ᗮ

noncomputable def HCPolySupport.PotentialSolenoidalExact.solenoidalZeroNormalTrace {d : ℕ} (U : Set (Vec d)) : Submodule ℝ ↥(HilbertVectorL2 U)

The generic orthogonal complement of all potential fields, i.e. fields with zero normal trace in the Chapter 1 terminology. The source-facing facade is Book.Ch01.SolenoidalZeroNormalTraceHilbertL2.

Equations

• HCPolySupport.PotentialSolenoidalExact.solenoidalZeroNormalTrace U = (HCPolySupport.PotentialSolenoidalExact.potential U)ᗮ

noncomputable def HCPolySupport.PotentialSolenoidalExact.blockPotentialSolenoidal {d : ℕ} (U : Set (Vec d)) : Submodule ℝ (↥(HilbertVectorL2 U) × ↥(HilbertVectorL2 U))

The generic literal doubled space L_pot(U) × L_sol(U). The Chapter 1 source-facing facade is Book.Ch01.PotentialSolenoidalHilbertL2.

Equations

• HCPolySupport.PotentialSolenoidalExact.blockPotentialSolenoidal U = (HCPolySupport.PotentialSolenoidalExact.potential U).prod (HCPolySupport.PotentialSolenoidalExact.solenoidal U)

noncomputable def HCPolySupport.PotentialSolenoidalExact.blockPotentialZeroTraceSolenoidalZeroNormalTrace {d : ℕ} (U : Set (Vec d)) : Submodule ℝ (↥(HilbertVectorL2 U) × ↥(HilbertVectorL2 U))

The generic literal doubled space L_pot,0(U) × L_sol,0(U). The Chapter 1 source-facing facade is Book.Ch01.PotentialZeroTraceSolenoidalZeroNormalTraceHilbertL2.

Equations

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

theorem HCPolySupport.PotentialSolenoidalExact.mem_potential_iff {d : ℕ} {U : Set (Vec d)} (g : ↥(HilbertVectorL2 U)) : g ∈ potential U ↔ ∃ (u : H1Function U), u.gradToHilbertVectorL2 = g

theorem HCPolySupport.PotentialSolenoidalExact.mem_potentialZeroTrace_iff {d : ℕ} {U : Set (Vec d)} (g : ↥(HilbertVectorL2 U)) : g ∈ potentialZeroTrace U ↔ ∃ (u : H10Function U), u.gradToHilbertVectorL2 = g

theorem HCPolySupport.PotentialSolenoidalExact.mem_solenoidal_iff {d : ℕ} {U : Set (Vec d)} (g : ↥(HilbertVectorL2 U)) : g ∈ solenoidal U ↔ ∀ (u : H10Function U), inner ℝ g u.gradToHilbertVectorL2 = 0

theorem HCPolySupport.PotentialSolenoidalExact.mem_solenoidalZeroNormalTrace_iff {d : ℕ} {U : Set (Vec d)} (g : ↥(HilbertVectorL2 U)) : g ∈ solenoidalZeroNormalTrace U ↔ ∀ (u : H1Function U), inner ℝ g u.gradToHilbertVectorL2 = 0

theorem HCPolySupport.PotentialSolenoidalExact.potentialZeroTrace_le_potential {d : ℕ} {U : Set (Vec d)} : potentialZeroTrace U ≤ potential U

theorem HCPolySupport.PotentialSolenoidalExact.solenoidalZeroNormalTrace_le_solenoidal {d : ℕ} {U : Set (Vec d)} : solenoidalZeroNormalTrace U ≤ solenoidal U

theorem HCPolySupport.PotentialSolenoidalExact.mem_blockPotentialSolenoidal_iff {d : ℕ} {U : Set (Vec d)} (g : ↥(HilbertVectorL2 U) × ↥(HilbertVectorL2 U)) : g ∈ blockPotentialSolenoidal U ↔ g.1 ∈ potential U ∧ g.2 ∈ solenoidal U

theorem HCPolySupport.PotentialSolenoidalExact.mem_blockPotentialZeroTraceSolenoidalZeroNormalTrace_iff {d : ℕ} {U : Set (Vec d)} (g : ↥(HilbertVectorL2 U) × ↥(HilbertVectorL2 U)) : g ∈ blockPotentialZeroTraceSolenoidalZeroNormalTrace U ↔ g.1 ∈ potentialZeroTrace U ∧ g.2 ∈ solenoidalZeroNormalTrace U

theorem HCPolySupport.PotentialSolenoidalExact.integral_eq_zero_of_mem_solenoidalZeroNormalTrace {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (g : ↥(HilbertVectorL2 U)) (hg : g ∈ solenoidalZeroNormalTrace U) : ∫ (x : Vec d), ↑↑g x ∂volumeMeasureOn U = 0

A zero-normal-trace solenoidal field has zero (restricted-volume) integral. The proof tests against affine H¹ functions with arbitrary constant gradient.

theorem HCPolySupport.PotentialSolenoidalExact.average_eq_zero_of_mem_solenoidalZeroNormalTrace {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (hne : U.Nonempty) (g : ↥(HilbertVectorL2 U)) (hg : g ∈ solenoidalZeroNormalTrace U) : (hU.toBoundedMeasurableDomain hne).average ↑↑g ⋯ = 0

The normalized-domain average of a zero-normal-trace solenoidal field vanishes.