Coarse-graining support: Support.Sobolev.PotentialSolenoidal

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

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

The vector field is the chosen weak gradient of an H¹ function on U.

Equations

• HCPolySupport.IsPotentialOn U f = ∃ (u : HCPolySupport.H1Function U), u.grad = f

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

The vector field is the chosen weak gradient of a zero-trace H¹ function on U.

Equations

• HCPolySupport.IsPotentialZeroTraceOn U f = ∃ (u : HCPolySupport.H10Function U), u.grad = f

noncomputable def HCPolySupport.IsSolenoidalOn {d : ℕ} (U : Set (Vec d)) (g : Vec d → Vec d) : Prop

The integral pairing of g with every zero-trace H¹ gradient on U vanishes.

Equations

• HCPolySupport.IsSolenoidalOn U g = ∀ (φ : HCPolySupport.H10Function U), ∫ (x : HCPolySupport.Vec d) in U, HCPolySupport.vecDot (g x) (φ.grad x) = 0

noncomputable def HCPolySupport.IsSolenoidalZeroNormalTraceOn {d : ℕ} (U : Set (Vec d)) (g : Vec d → Vec d) : Prop

The integral pairing of g with every H¹ gradient on U vanishes, expressing the solenoidal zero-normal-trace condition.

Equations

• HCPolySupport.IsSolenoidalZeroNormalTraceOn U g = ∀ (φ : HCPolySupport.H1Function U), ∫ (x : HCPolySupport.Vec d) in U, HCPolySupport.vecDot (g x) (φ.grad x) = 0

theorem HCPolySupport.H1Function.isPotentialOn {d : ℕ} {U : Set (Vec d)} (u : H1Function U) : IsPotentialOn U u.grad

theorem HCPolySupport.H10Function.isPotentialZeroTraceOn {d : ℕ} {U : Set (Vec d)} (u : H10Function U) : IsPotentialZeroTraceOn U u.grad

theorem HCPolySupport.IsPotentialZeroTraceOn.congr_ae {d : ℕ} {U : Set (Vec d)} {f g : Vec d → Vec d} (hfg : f =ᵐ[MeasureTheory.volume.restrict U] g) (hf : IsPotentialZeroTraceOn U f) : IsPotentialZeroTraceOn U g

The zero-trace potential predicate is insensitive to changing the vector field on a null set. This is the representative bridge needed when moving from closed L² subspaces back to witness-based Sobolev predicates.

theorem HCPolySupport.IsPotentialZeroTraceOn.isPotentialOn {d : ℕ} {U : Set (Vec d)} {f : Vec d → Vec d} (hf : IsPotentialZeroTraceOn U f) : IsPotentialOn U f

theorem HCPolySupport.isPotentialOn_zero {d : ℕ} {U : Set (Vec d)} : IsPotentialOn U 0

theorem HCPolySupport.isPotentialOn_add {d : ℕ} {U : Set (Vec d)} {f g : Vec d → Vec d} (hf : IsPotentialOn U f) (hg : IsPotentialOn U g) : IsPotentialOn U (f + g)

theorem HCPolySupport.isPotentialOn_smul {d : ℕ} {U : Set (Vec d)} {f : Vec d → Vec d} (hf : IsPotentialOn U f) (c : ℝ) : IsPotentialOn U (c • f)

theorem HCPolySupport.isPotentialZeroTraceOn_zero {d : ℕ} {U : Set (Vec d)} : IsPotentialZeroTraceOn U 0

theorem HCPolySupport.isPotentialZeroTraceOn_add {d : ℕ} {U : Set (Vec d)} {f g : Vec d → Vec d} (hf : IsPotentialZeroTraceOn U f) (hg : IsPotentialZeroTraceOn U g) : IsPotentialZeroTraceOn U (f + g)

theorem HCPolySupport.isPotentialZeroTraceOn_smul {d : ℕ} {U : Set (Vec d)} {f : Vec d → Vec d} (hf : IsPotentialZeroTraceOn U f) (c : ℝ) : IsPotentialZeroTraceOn U (c • f)

theorem HCPolySupport.isPotentialOn_of_contDiff {d : ℕ} {U : Set (Vec d)} (hU : IsOpen U) {u : Vec d → ℝ} (hu : ContDiff ℝ 1 u) (hu_supp : HasCompactSupport u) : IsPotentialOn U fun (x : Vec d) (i : Fin d) => (fderiv ℝ u x) (basisVec i)

theorem HCPolySupport.isPotentialZeroTraceOn_of_contDiff {d : ℕ} {U : Set (Vec d)} (hU : IsOpen U) {u : Vec d → ℝ} (hu : ContDiff ℝ (↑⊤) u) (hu_supp : HasCompactSupport u) (hu_sub : tsupport u ⊆ U) : IsPotentialZeroTraceOn U fun (x : Vec d) (i : Fin d) => (fderiv ℝ u x) (basisVec i)

theorem HCPolySupport.isSolenoidalOn_zero {d : ℕ} {U : Set (Vec d)} : IsSolenoidalOn U 0

theorem HCPolySupport.isSolenoidalOn_add {d : ℕ} {U : Set (Vec d)} {f g : Vec d → Vec d} (hf : IsSolenoidalOn U f) (hg : IsSolenoidalOn U g) (hf_int : ∀ (φ : H10Function U), MeasureTheory.IntegrableOn (fun (x : Vec d) => vecDot (f x) (φ.grad x)) U MeasureTheory.volume) (hg_int : ∀ (φ : H10Function U), MeasureTheory.IntegrableOn (fun (x : Vec d) => vecDot (g x) (φ.grad x)) U MeasureTheory.volume) : IsSolenoidalOn U (f + g)

theorem HCPolySupport.isSolenoidalOn_smul {d : ℕ} {U : Set (Vec d)} {g : Vec d → Vec d} (hg : IsSolenoidalOn U g) (c : ℝ) : IsSolenoidalOn U (c • g)

theorem HCPolySupport.isSolenoidalZeroNormalTraceOn_zero {d : ℕ} {U : Set (Vec d)} : IsSolenoidalZeroNormalTraceOn U 0

theorem HCPolySupport.isSolenoidalZeroNormalTraceOn_add {d : ℕ} {U : Set (Vec d)} {f g : Vec d → Vec d} (hf : IsSolenoidalZeroNormalTraceOn U f) (hg : IsSolenoidalZeroNormalTraceOn U g) (hf_int : ∀ (φ : H1Function U), MeasureTheory.IntegrableOn (fun (x : Vec d) => vecDot (f x) (φ.grad x)) U MeasureTheory.volume) (hg_int : ∀ (φ : H1Function U), MeasureTheory.IntegrableOn (fun (x : Vec d) => vecDot (g x) (φ.grad x)) U MeasureTheory.volume) : IsSolenoidalZeroNormalTraceOn U (f + g)

theorem HCPolySupport.isSolenoidalZeroNormalTraceOn_smul {d : ℕ} {U : Set (Vec d)} {g : Vec d → Vec d} (hg : IsSolenoidalZeroNormalTraceOn U g) (c : ℝ) : IsSolenoidalZeroNormalTraceOn U (c • g)

theorem HCPolySupport.IsSolenoidalOn.test_of_contDiff {d : ℕ} {U : Set (Vec d)} {g : Vec d → Vec d} (hg : IsSolenoidalOn U g) (hU : IsOpen U) {u : Vec d → ℝ} (hu : ContDiff ℝ (↑⊤) u) (hu_supp : HasCompactSupport u) (hu_sub : tsupport u ⊆ U) : (∫ (x : Vec d) in U, vecDot (g x) fun (i : Fin d) => (fderiv ℝ u x) (basisVec i)) = 0

theorem HCPolySupport.IsSolenoidalZeroNormalTraceOn.test_of_contDiff {d : ℕ} {U : Set (Vec d)} {g : Vec d → Vec d} (hg : IsSolenoidalZeroNormalTraceOn U g) (hU : IsOpen U) {u : Vec d → ℝ} (hu : ContDiff ℝ 1 u) (hu_supp : HasCompactSupport u) : (∫ (x : Vec d) in U, vecDot (g x) fun (i : Fin d) => (fderiv ℝ u x) (basisVec i)) = 0