Project documentation
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.
Exact Lean statement
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 : (Fin d → ℝ) →ₘ[μU d U] ℝ) : (Fin d → ℝ) → ℝ)
=ᵐ[volume.restrict U]
((Df2 : (Fin d → ℝ) →ₘ[μU d U] ℝ) : (Fin d → ℝ) → ℝ)Formal artifact
Lean source
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 : (Fin d → ℝ) →ₘ[μU d U] ℝ) : (Fin d → ℝ) → ℝ) =ᵐ[volume.restrict U] ((Df2 : (Fin d → ℝ) →ₘ[μU d U] ℝ) : (Fin d → ℝ) → ℝ) := by classical have LocIntDf1 := by simpa using LplocLocallyIntegU d 1 (le_refl 1) U hU Df1.prop have LocIntDf2 := by simpa using LplocLocallyIntegU d 1 (le_refl 1) U hU Df2.prop apply IsOpen.ae_eq_of_integral_contDiff_smul_eq (hU := hU) (hf := LocIntDf1) (hg := LocIntDf2) intro ψ hψ have := h2 ψ hψ; rw [h1 ψ hψ] at this rw [integral_muU_eq_volume_of_Cc hU hψ (Df1), integral_muU_eq_volume_of_Cc hU hψ (Df2)] at this simpa using this- Project
- PDE
- License
- Apache-2.0
- Commit
- 0ab5d79a0d7a
- Source
- PDE/SobolevSpace/WeakDerivative.lean:131-149
Reuse this declaration
Bring the exact result into your workflow
The import identifies the source module. Your project still needs the pinned package dependency shown on this page.
What this badge means
This completion status comes from the project or community source. It has not yet been represented here as an independent rebuild and axiom audit.
Continue in this project
Related declarations
Fderiv Ccinfty
FderivCcinfty
Plain-language statement
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.
Source project: PDE
Person-level attribution pending.
Heat from convolution heat Kernel
heat_from_convolution_heatKernel
Project documentation
Swap the second spatial derivative with the integral . -/ lemma swap_xx_heatKernel {α : ℝ} {x t : ℝ} (g : ℝ → ℝ) (ht : 0 < t) (hα : 0 < α) (hg : Integrable g) : HasDerivAt (fun x' => ∫ y, HKx α (x' - y) t * g y ∂volume) (∫ y, HKxx α (x - y) t * g y ∂volume) x := by have mem_nhds : Metric.ball x 1 ∈ 𝓝 x := Metric.ball_mem_nhds x (by...
Source project: PDE
Person-level attribution pending.
Deriv exp heat Kernel
Heat.deriv_exp_heatKernel
Plain-language statement
Derivative of the exponential term exp(-(x²)/(4αt)) with respect to x.
Source project: PDE
Person-level attribution pending.