Coarse-graining support: Support.Book.Ch01.FieldSpaces

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

Chapter 1 public field-space predicates

This module exposes the literal Hilbert-space potential/solenoidal quartet on nonempty bounded open convex domains, together with representative-level predicates retained for statements formulated for concrete functions.

@[reducible, inline]

noncomputable abbrev HCPolySupport.Book.Ch01.PotentialHilbertL2 {d : ℕ} (U : Set (Vec d)) (hU : IsOpenBoundedConvexDomain U) (hne : U.Nonempty) : Submodule ℝ ↥(HilbertVectorL2 U)

The literal range of H¹(U) gradients in HilbertVectorL2 U.

The domain hypotheses are part of the Chapter 1 facade; the underlying exact submodule construction itself is available on an arbitrary carrier.

Equations

• HCPolySupport.Book.Ch01.PotentialHilbertL2 U hU hne = HCPolySupport.PotentialSolenoidalExact.potential U

@[reducible, inline]

noncomputable abbrev HCPolySupport.Book.Ch01.PotentialZeroTraceHilbertL2 {d : ℕ} (U : Set (Vec d)) (hU : IsOpenBoundedConvexDomain U) (hne : U.Nonempty) : Submodule ℝ ↥(HilbertVectorL2 U)

The literal range of H¹₀(U) gradients in HilbertVectorL2 U.

Equations

• HCPolySupport.Book.Ch01.PotentialZeroTraceHilbertL2 U hU hne = HCPolySupport.PotentialSolenoidalExact.potentialZeroTrace U

@[reducible, inline]

noncomputable abbrev HCPolySupport.Book.Ch01.SolenoidalHilbertL2 {d : ℕ} (U : Set (Vec d)) (hU : IsOpenBoundedConvexDomain U) (hne : U.Nonempty) : Submodule ℝ ↥(HilbertVectorL2 U)

The exact solenoidal submodule, orthogonal to PotentialZeroTraceHilbertL2.

Equations

• HCPolySupport.Book.Ch01.SolenoidalHilbertL2 U hU hne = HCPolySupport.PotentialSolenoidalExact.solenoidal U

@[reducible, inline]

noncomputable abbrev HCPolySupport.Book.Ch01.SolenoidalZeroNormalTraceHilbertL2 {d : ℕ} (U : Set (Vec d)) (hU : IsOpenBoundedConvexDomain U) (hne : U.Nonempty) : Submodule ℝ ↥(HilbertVectorL2 U)

The exact zero-normal-trace solenoidal submodule, orthogonal to PotentialHilbertL2.

Equations

• HCPolySupport.Book.Ch01.SolenoidalZeroNormalTraceHilbertL2 U hU hne = HCPolySupport.PotentialSolenoidalExact.solenoidalZeroNormalTrace U

@[reducible, inline]

noncomputable abbrev HCPolySupport.Book.Ch01.PotentialSolenoidalHilbertL2 {d : ℕ} (U : Set (Vec d)) (hU : IsOpenBoundedConvexDomain U) (hne : U.Nonempty) : Submodule ℝ (↥(HilbertVectorL2 U) × ↥(HilbertVectorL2 U))

The exact doubled submodule PotentialHilbertL2 U hU hne × SolenoidalHilbertL2 U hU hne.

Equations

• HCPolySupport.Book.Ch01.PotentialSolenoidalHilbertL2 U hU hne = HCPolySupport.PotentialSolenoidalExact.blockPotentialSolenoidal U

@[reducible, inline]

noncomputable abbrev HCPolySupport.Book.Ch01.PotentialZeroTraceSolenoidalZeroNormalTraceHilbertL2 {d : ℕ} (U : Set (Vec d)) (hU : IsOpenBoundedConvexDomain U) (hne : U.Nonempty) : Submodule ℝ (↥(HilbertVectorL2 U) × ↥(HilbertVectorL2 U))

The exact doubled submodule PotentialZeroTraceHilbertL2 U hU hne × SolenoidalZeroNormalTraceHilbertL2 U hU hne.

Equations

• HCPolySupport.Book.Ch01.PotentialZeroTraceSolenoidalZeroNormalTraceHilbertL2 U hU hne = HCPolySupport.PotentialSolenoidalExact.blockPotentialZeroTraceSolenoidalZeroNormalTrace U

theorem HCPolySupport.Book.Ch01.mem_potentialHilbertL2_iff {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (hne : U.Nonempty) (g : ↥(HilbertVectorL2 U)) : g ∈ PotentialHilbertL2 U hU hne ↔ ∃ (u : H1Function U), u.gradToHilbertVectorL2 = g

theorem HCPolySupport.Book.Ch01.mem_potentialZeroTraceHilbertL2_iff {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (hne : U.Nonempty) (g : ↥(HilbertVectorL2 U)) : g ∈ PotentialZeroTraceHilbertL2 U hU hne ↔ ∃ (u : H10Function U), u.gradToHilbertVectorL2 = g

theorem HCPolySupport.Book.Ch01.mem_solenoidalHilbertL2_iff {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (hne : U.Nonempty) (g : ↥(HilbertVectorL2 U)) : g ∈ SolenoidalHilbertL2 U hU hne ↔ ∀ (u : H10Function U), inner ℝ g u.gradToHilbertVectorL2 = 0

theorem HCPolySupport.Book.Ch01.mem_solenoidalZeroNormalTraceHilbertL2_iff {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (hne : U.Nonempty) (g : ↥(HilbertVectorL2 U)) : g ∈ SolenoidalZeroNormalTraceHilbertL2 U hU hne ↔ ∀ (u : H1Function U), inner ℝ g u.gradToHilbertVectorL2 = 0

theorem HCPolySupport.Book.Ch01.potentialZeroTraceHilbertL2_le_potentialHilbertL2 {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (hne : U.Nonempty) : PotentialZeroTraceHilbertL2 U hU hne ≤ PotentialHilbertL2 U hU hne

theorem HCPolySupport.Book.Ch01.solenoidalZeroNormalTraceHilbertL2_le_solenoidalHilbertL2 {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (hne : U.Nonempty) : SolenoidalZeroNormalTraceHilbertL2 U hU hne ≤ SolenoidalHilbertL2 U hU hne

theorem HCPolySupport.Book.Ch01.mem_potentialSolenoidalHilbertL2_iff {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (hne : U.Nonempty) (g : ↥(HilbertVectorL2 U) × ↥(HilbertVectorL2 U)) : g ∈ PotentialSolenoidalHilbertL2 U hU hne ↔ g.1 ∈ PotentialHilbertL2 U hU hne ∧ g.2 ∈ SolenoidalHilbertL2 U hU hne

theorem HCPolySupport.Book.Ch01.mem_potentialZeroTraceSolenoidalZeroNormalTraceHilbertL2_iff {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (hne : U.Nonempty) (g : ↥(HilbertVectorL2 U) × ↥(HilbertVectorL2 U)) : g ∈ PotentialZeroTraceSolenoidalZeroNormalTraceHilbertL2 U hU hne ↔ g.1 ∈ PotentialZeroTraceHilbertL2 U hU hne ∧ g.2 ∈ SolenoidalZeroNormalTraceHilbertL2 U hU hne

theorem HCPolySupport.Book.Ch01.integral_eq_zero_of_mem_solenoidalZeroNormalTraceHilbertL2 {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (hne : U.Nonempty) (g : ↥(HilbertVectorL2 U)) (hg : g ∈ SolenoidalZeroNormalTraceHilbertL2 U hU hne) : ∫ (x : Vec d), ↑↑g x ∂volumeMeasureOn U = 0

A field in the manuscript space L_sol,0(U) has zero restricted-volume integral.

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

The normalized-domain average of a field in the manuscript space L_sol,0(U) vanishes.

def HCPolySupport.Book.Ch01.PotentialFieldOn {d : ℕ} (U : Set (Vec d)) (f : Vec d → Vec d) : Prop

Representative-level L² potential predicate on U, stated up to a.e. equality. The literal Hilbert-space submodule is PotentialHilbertL2.

Equations

• HCPolySupport.Book.Ch01.PotentialFieldOn U f = (HCPolySupport.MemVectorL2 U f ∧ ∃ (u : HCPolySupport.H1Function U), f =ᵐ[HCPolySupport.volumeMeasureOn U] u.grad)

def HCPolySupport.Book.Ch01.PotentialZeroTraceFieldOn {d : ℕ} (U : Set (Vec d)) (f : Vec d → Vec d) : Prop

Representative-level zero-trace L² potential predicate on U, stated up to a.e. equality. The literal Hilbert-space submodule is PotentialZeroTraceHilbertL2.

Equations

• HCPolySupport.Book.Ch01.PotentialZeroTraceFieldOn U f = (HCPolySupport.MemVectorL2 U f ∧ ∃ (u : HCPolySupport.H10Function U), f =ᵐ[HCPolySupport.volumeMeasureOn U] u.grad)

@[reducible, inline]

abbrev HCPolySupport.Book.Ch01.LocalizedZeroTraceFunctionOn {d : ℕ} (Ω V : Set (Vec d)) (u : Vec d → ℝ) : Prop

Public localized scalar zero-trace condition.

This is the a.e./Sobolev replacement for saying that a scalar function vanishes on the part of ∂Ω seen through the localization window V: every smooth compactly supported cutoff localized in V turns the function into an admissible H¹₀(Ω) test function.

Equations

• HCPolySupport.Book.Ch01.LocalizedZeroTraceFunctionOn Ω V u = HCPolySupport.LocalizedZeroTraceFunctionOn Ω V u

def HCPolySupport.Book.Ch01.SolenoidalFieldOn {d : ℕ} (U : Set (Vec d)) (g : Vec d → Vec d) : Prop

Representative-level L² solenoidal predicate on U. The integral formulation is a.e.-insensitive once the L² representative is fixed; the literal Hilbert-space submodule is SolenoidalHilbertL2.

Equations

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

def HCPolySupport.Book.Ch01.SolenoidalZeroNormalTraceFieldOn {d : ℕ} (U : Set (Vec d)) (g : Vec d → Vec d) : Prop

Representative-level L² solenoidal predicate with zero normal trace on U. The literal Hilbert-space submodule is SolenoidalZeroNormalTraceHilbertL2.

Equations

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