Project-declaredLean 4.30.0 · mathlib@c5ea00351c28

Wkp UNorm eq zero iff

WkpUNorm_eq_zero_iff

partial differential equations Sobolev spaces analysis sobolev spaces

Plain-language statement

The W^{k,p}(U) norm vanishes iff the function is zero a.e..

Exact Lean statement

lemma WkpUNorm_eq_zero_iff (hp : 1 ≤ p) {f : WkpU d k p U hU} :
    WkpUNorm k p f = 0 ↔ f.val.val =ᵐ[μU d U] 0

Formal artifact

Lean source

Canonical source

Full Lean sourceLean 4

lemma WkpUNorm_eq_zero_iff (hp : 1 ≤ p) {f : WkpU d k p U hU} :    WkpUNorm k p f = 0 ↔ f.val.val =ᵐ[μU d U] 0 := by  have hp0 : p ≠ 0 := (one_pos.trans_le hp).ne'  rw [WkpUNorm_eq_zero_iff']  constructor  · intro hf    have h0 : eLpNorm (f.val : (Fin d → ℝ) → ℝ) p (μU d U) = 0 := by      simp only [WkpU.eNorm] at hf      split_ifs at hf with hpt      · exact ENNReal.iSup_eq_zero.mp          (ENNReal.iSup_eq_zero.mp hf ⟨0, k.succ_pos⟩) Fin.elim0      · rcases ENNReal.rpow_eq_zero_iff.mp hf with ⟨hS, _⟩ | ⟨_, h⟩        · exact (ENNReal.rpow_eq_zero_iff_of_pos (ENNReal.toReal_pos hp0 hpt)).mp              (Finset.sum_eq_zero_iff.mp                (Finset.sum_eq_zero_iff.mp hS ⟨0, k.succ_pos⟩ (Finset.mem_univ _))                Fin.elim0 (Finset.mem_univ _))        · exact absurd h (not_lt.mpr (by positivity))    exact (eLpNorm_eq_zero_iff (WkpU.aestronglyMeasurable f) hp0).mp h0  · exact fun hf => WkpU.eNorm_eq_zero_of_ae_zero hp0 f hf

Project: PDE
License: Apache-2.0
Commit: 0ab5d79a0d7a
Source: PDE/SobolevSpace/SobolevSpaces.lean:230-248

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

Project-declaredLean 4.30.0

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.

partial differential equationsSobolev spacesanalysis

Source project: PDE

Person-level attribution pending.

View proof record

Project-declaredLean 4.30.0

Heat from convolution heat Kernel

heat_from_convolution_heatKernel

Project documentation

Swap the second spatial derivative $\partial_{xx}$ with the integral $\int$ . -/ 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...

partial differential equationsSobolev spacesanalysis

Source project: PDE

Person-level attribution pending.

View proof record

Project-declaredLean 4.30.0

Deriv exp heat Kernel

Heat.deriv_exp_heatKernel

Plain-language statement

Derivative of the exponential term exp(-(x²)/(4αt)) with respect to x.

partial differential equationsSobolev spacesanalysis

Source project: PDE

Person-level attribution pending.

View proof record