def unitSeq {d : ℕ+} {n : ℕ} (s : Fin n → Fin ↑d) : Fin n → Fin ↑d → ℝ

Standard basis vector sequence in ℝᵈ indexed by s : Fin n → Fin d, used to evaluate iterated Fréchet derivatives along coordinate directions.

Equations

• unitSeq s j = Pi.single (s j) 1

theorem IntMulLocalintComp {d : ℕ+} (U : Set (Fin ↑d → ℝ)) {f : (Fin ↑d → ℝ) →ₘ[MeasureTheory.volume] ℝ} {ψ : (Fin ↑d → ℝ) → ℝ} (hf : MeasureTheory.LocallyIntegrableOn (↑f) U MeasureTheory.volume) (ψ_comp : HasCompactSupport ψ) (ψ_supp : tsupport ψ ⊆ U) (ψ_cont : Continuous ψ) : MeasureTheory.Integrable (fun (x : Fin ↑d → ℝ) => ψ x * ↑f x) MeasureTheory.volume

If f is locally integrable on U and ψ ∈ Cc^∞(U), then ψ · f is integrable on all of ℝᵈ. This is the key integrability bridge between local and global theories.

theorem FderivCcinfty {d : ℕ+} {n : ℕ} {U : Set (Fin ↑d → ℝ)} (s : Fin n → Fin ↑d) {ψ : (Fin ↑d → ℝ) → ℝ} (hψ : ψ ∈ Cc_inftyU d U) : (fun (x : Fin ↑d → ℝ) => (iteratedFDeriv ℝ n ψ x) (unitSeq s)) ∈ Cc_inftyU d U

The Fréchet derivative x ↦ (∂ˢψ(x))(unitSeq s) of a test function ψ ∈ Cc^∞(U) again lies in Cc^∞(U). This is used to compose the weak derivative definition with itself.

theorem IsOpen.ae_eq_of_integral_contDiff_smul_eq {d : ℕ+} {U : Set (Fin ↑d → ℝ)} {hU : IsOpen U} {f g : (Fin ↑d → ℝ) →ₘ[MeasureTheory.volume] ℝ} {hf : MeasureTheory.LocallyIntegrableOn (↑f) U MeasureTheory.volume} {hg : MeasureTheory.LocallyIntegrableOn (↑g) U MeasureTheory.volume} (h : ∀ ψ ∈ Cc_inftyU d U, ∫ (x : Fin ↑d → ℝ), ψ x • ↑f x = ∫ (x : Fin ↑d → ℝ), ψ x • ↑g x) : ↑f =ᵐ[MeasureTheory.volume.restrict U] ↑g

If ∫ ψ · f = ∫ ψ · g for all ψ ∈ Cc^∞(U), then f =ᵃᵉ g on U. This is the du Bois-Reymond lemma, the key uniqueness engine for weak derivatives.

noncomputable def IsWeakMultiDerivU {d : ℕ+} {n : ℕ} (U : Set (Fin ↑d → ℝ)) (s : Fin n → Fin ↑d) (f Df : ↥(Lp_locU d 1 U)) : Prop

IsWeakMultiDerivU U s f Df asserts that Df is the weak derivative of f in the directions encoded by s : Fin n → Fin d on the open set U: ∫_U f · ∂ˢψ = (-1)ⁿ · ∫_U Df · ψ for all test functions ψ ∈ Cc^∞(U).

Equations

• IsWeakMultiDerivU U s f Df = ∀ ψ ∈ Cc_inftyU d U, ∫ (x : Fin ↑d → ℝ), ↑↑f x • (iteratedFDeriv ℝ n ψ x) (unitSeq s) = (-1) ^ n • ∫ (x : Fin ↑d → ℝ), ψ x • ↑↑Df x

@[simp]

theorem isWeakMultiDerivU_iff {d : ℕ+} {n : ℕ} {U : Set (Fin ↑d → ℝ)} {s : Fin n → Fin ↑d} {f Df : ↥(Lp_locU d 1 U)} : IsWeakMultiDerivU U s f Df ↔ ∀ ψ ∈ Cc_inftyU d U, ∫ (x : Fin ↑d → ℝ), ↑↑f x • (iteratedFDeriv ℝ n ψ x) (unitSeq s) = (-1) ^ n • ∫ (x : Fin ↑d → ℝ), ψ x • ↑↑Df x

noncomputable def HasWeakMultiDerivU {d : ℕ+} {n : ℕ} (U : Set (Fin ↑d → ℝ)) (f : ↥(Lp_locU d 1 U)) (s : Fin n → Fin ↑d) : Prop

f has a weak multi-derivative in directions s on U if there exists a locally integrable function satisfying the integration-by-parts identity.

Equations

• HasWeakMultiDerivU U f s = ∃ (Df : ↥(Lp_locU d 1 U)), IsWeakMultiDerivU U s f Df

theorem WeakDerivUniqU {d : ℕ+} {n : ℕ} {U : Set (Fin ↑d → ℝ)} (hU : IsOpen U) {f : ↥(Lp_locU d 1 U)} {s : Fin n → Fin ↑d} {Df1 Df2 : ↥(Lp_locU d 1 U)} (h1 : IsWeakMultiDerivU U s f Df1) (h2 : IsWeakMultiDerivU U s f Df2) : ↑↑Df1 =ᵐ[MeasureTheory.volume.restrict U] ↑↑Df2

Uniqueness of weak multi-derivatives on U: any two candidates must agree almost everywhere on U. The proof reduces to the du Bois-Reymond lemma via the defining identity.

noncomputable def WeakmultiderivU {d : ℕ+} {n : ℕ} (U : Set (Fin ↑d → ℝ)) (f : ↥(Lp_locU d 1 U)) (s : Fin n → Fin ↑d) (h : HasWeakMultiDerivU U f s) : ↥(Lp_locU d 1 U)

The canonical weak multi-derivative on U, chosen by Classical.choose.

Equations

• WeakmultiderivU U f s h = Classical.choose h

theorem WeakmultiderivU_spec {d : ℕ+} {n : ℕ} (U : Set (Fin ↑d → ℝ)) (f : ↥(Lp_locU d 1 U)) (s : Fin n → Fin ↑d) (h : HasWeakMultiDerivU U f s) : IsWeakMultiDerivU U s f (WeakmultiderivU U f s h)

theorem WeakmultiderivU_unique {d : ℕ+} {n : ℕ} {U : Set (Fin ↑d → ℝ)} (hU : IsOpen U) (s : Fin n → Fin ↑d) (f : ↥(Lp_locU d 1 U)) (h : HasWeakMultiDerivU U f s) (Df : ↥(Lp_locU d 1 U)) (hDf : IsWeakMultiDerivU U s f Df) : ↑↑(WeakmultiderivU U f s h) =ᵐ[MeasureTheory.volume.restrict U] ↑↑Df

Any weak multi-derivative Df on U agrees a.e. with the canonical choice.

theorem zeroWeakmultiDerivU {d : ℕ+} {n : ℕ} (U : Set (Fin ↑d → ℝ)) (hU : IsOpen U) (s : Fin n → Fin ↑d) : ∃ (h : HasWeakMultiDerivU U 0 s), ↑↑(WeakmultiderivU U 0 s h) =ᵐ[MeasureTheory.volume.restrict U] ↑0

theorem WeakmultiDerivU_add {d : ℕ+} {n : ℕ} (U : Set (Fin ↑d → ℝ)) (hU : IsOpen U) (s : Fin n → Fin ↑d) (f g : ↥(Lp_locU d 1 U)) (hf : HasWeakMultiDerivU U f s) (hg : HasWeakMultiDerivU U g s) : ∃ (h_add : HasWeakMultiDerivU U (f + g) s), ↑↑(WeakmultiderivU U (f + g) s h_add) =ᵐ[MeasureTheory.volume.restrict U] ↑(↑(WeakmultiderivU U f s hf) + ↑(WeakmultiderivU U g s hg))

theorem WeakmultiDerivU_smul {d : ℕ+} {n : ℕ} (U : Set (Fin ↑d → ℝ)) (hU : IsOpen U) (s : Fin n → Fin ↑d) (f : ↥(Lp_locU d 1 U)) (c : ℝ) (hf : HasWeakMultiDerivU U f s) : ∃ (h_smul : HasWeakMultiDerivU U (c • f) s), ↑↑(WeakmultiderivU U (c • f) s h_smul) =ᵐ[MeasureTheory.volume.restrict U] ↑(c • ↑(WeakmultiderivU U f s hf))

@[reducible, inline]

noncomputable abbrev IsWeakMultiDeriv {d : ℕ+} {n : ℕ} (s : Fin n → Fin ↑d) (f Df : ↥(Lp_loc d 1)) : Prop

IsWeakMultiDeriv s f Df asserts that Df is the weak multi-derivative of f in directions s on all of ℝᵈ. Definitionally equal to IsWeakMultiDerivU Set.univ s f Df.

Equations

• IsWeakMultiDeriv s f Df = IsWeakMultiDerivU Set.univ s f Df

@[reducible, inline]

noncomputable abbrev HasWeakMultiDeriv {d : ℕ+} {n : ℕ} (f : ↥(Lp_loc d 1)) (s : Fin n → Fin ↑d) : Prop

f has a weak multi-derivative in directions s on ℝᵈ.

Equations

• HasWeakMultiDeriv f s = HasWeakMultiDerivU Set.univ f s

theorem WeakDerivUniq {d : ℕ+} {n : ℕ} {f : ↥(Lp_loc d 1)} {s : Fin n → Fin ↑d} {Df1 Df2 : ↥(Lp_loc d 1)} (h1 : IsWeakMultiDeriv s f Df1) (h2 : IsWeakMultiDeriv s f Df2) : ↑↑Df1 =ᵐ[MeasureTheory.volume] ↑↑Df2

Uniqueness of weak multi-derivatives on ℝᵈ: follows from WeakDerivUniqU applied to U = Set.univ. The a.e. equality is on volume rather than volume.restrict Set.univ.

@[reducible, inline]

noncomputable abbrev weakmultideriv {d : ℕ+} {n : ℕ} (f : ↥(Lp_loc d 1)) (s : Fin n → Fin ↑d) (h : HasWeakMultiDeriv f s) : ↥(Lp_loc d 1)

The canonical weak multi-derivative on ℝᵈ.

Equations

• weakmultideriv f s h = WeakmultiderivU Set.univ f s h

theorem weakmultideriv_spec {d : ℕ+} {n : ℕ} (f : ↥(Lp_loc d 1)) (s : Fin n → Fin ↑d) (h : HasWeakMultiDeriv f s) : IsWeakMultiDeriv s f (weakmultideriv f s h)

theorem weakmultideriv_unique {d : ℕ+} {n : ℕ} (s : Fin n → Fin ↑d) (f : ↥(Lp_loc d 1)) (h : HasWeakMultiDeriv f s) (Df : ↥(Lp_loc d 1)) (hDf : IsWeakMultiDeriv s f Df) : ↑↑(weakmultideriv f s h) =ᵐ[MeasureTheory.volume] ↑↑Df

Any weak multi-derivative Df on ℝᵈ agrees a.e. with the canonical choice.