Weak-gradient bridge

This module gives the integration-by-parts weak-gradient relation a distributional name. The test functions are bundled with their C¹, compact support, and support-in-domain data, so future mathlib distribution/test-function work has a single interface to refine.

structure LeanStationaryHarmonicMaps.StationaryHarmonicMap.CompactlySupportedC1In {n : ℕ} (Ω : Set (Domain n)) (F : Type u_1) [NormedAddCommGroup F] [NormedSpace ℝ F] : Type u_1

Bundled compactly supported C¹ test functions with topological support contained in the domain.

• toFun : Domain n → F

  The underlying function of a compactly supported C¹ test map.

• contDiff : ContDiff ℝ 1 self.toFun
• hasCompactSupport : HasCompactSupport self.toFun
• tsupport_subset : tsupport self.toFun ⊆ Ω

@[instance_reducible]

instance LeanStationaryHarmonicMaps.StationaryHarmonicMap.CompactlySupportedC1In.instCoeFunForallDomain {n : ℕ} {Ω : Set (Domain n)} {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] : CoeFun (CompactlySupportedC1In Ω F) fun (x : CompactlySupportedC1In Ω F) => Domain n → F

Equations

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

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.CompactlySupportedC1In.coe_mk {n : ℕ} {Ω : Set (Domain n)} {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (ψ : Domain n → F) (hψ : ContDiff ℝ 1 ψ) (hψ_compact : HasCompactSupport ψ) (hψ_support : tsupport ψ ⊆ Ω) : { toFun := ψ, contDiff := hψ, hasCompactSupport := hψ_compact, tsupport_subset := hψ_support }.toFun = ψ

structure LeanStationaryHarmonicMaps.StationaryHarmonicMap.DistributionalWeakGradientIn {n m : ℕ} (u : Domain n → Target m) (Du : Domain n → Gradient n m) (Ω : Set (Domain n)) : Prop

Distributional weak-gradient relation for a chosen gradient field.

• integration_by_parts (i : Fin n) (ψ : CompactlySupportedC1In Ω (Target m)) : ∫ (x : Domain n) in Ω, inner ℝ (u x) (partialDerivative ψ.toFun i x) = -∫ (x : Domain n) in Ω, inner ℝ (Du x i) (ψ.toFun x)

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.DistributionalWeakGradientIn.toHasWeakGradientIn {n m : ℕ} {u : Domain n → Target m} {Du : Domain n → Gradient n m} {Ω : Set (Domain n)} (h : DistributionalWeakGradientIn u Du Ω) : HasWeakGradientIn u Du Ω

The distributional weak-gradient bridge implies the custom weak-gradient interface used by the monotonicity proof.