Project-declaredLean 4.30.0 · mathlib@c5ea00351c28

Wkp U e Norm add le

WkpU.eNorm_add_le

partial differential equations Sobolev spaces analysis sobolev spaces

Plain-language statement

Triangle inequality for eLpNorm.

Exact Lean statement

lemma WkpU.eNorm_add_le {d : ℕ+} {k : ℕ} {p : ℝ≥0∞}
    {U : Set (Fin d → ℝ)} {hU : IsOpen U} (hp1 : 1 ≤ p)
    (f g : WkpU d k p U hU) :
    WkpU.eNorm k p (f + g) ≤ WkpU.eNorm k p f + WkpU.eNorm k p g

Formal artifact

Lean source

Canonical source

Full Lean sourceLean 4

lemma WkpU.eNorm_add_le {d : ℕ+} {k : ℕ} {p : ℝ≥0∞}    {U : Set (Fin d → ℝ)} {hU : IsOpen U} (hp1 : 1 ≤ p)    (f g : WkpU d k p U hU) :    WkpU.eNorm k p (f + g) ≤ WkpU.eNorm k p f + WkpU.eNorm k p g := by    unfold WkpU.eNorm    split_ifs with hp_top    · refine iSup_le fun n => iSup_le fun s => ?_      refine (WkpU.derivELpNorm_add_le hp1 f g n.val s).trans ?_      exact add_le_add (le_iSup_of_le n (le_iSup _ s)) (le_iSup_of_le n (le_iSup _ s))    · have hp_pos : 0 < p.toReal :=        ENNReal.toReal_pos (one_pos.trans_le hp1).ne' hp_top      let σ := Σ n : Fin (k + 1), Fin n.val → Fin d      have reindex  := fun h : WkpU d k p U hU =>        (Fintype.sum_sigma          (fun i : σ => WkpU.derivELpNorm h i.1.val i.2 ^ p.toReal)).symm      rw [reindex (f + g), reindex f, reindex g]      refine le_trans ?_        (ENNReal.Lp_add_le Finset.univ          (fun i : σ => WkpU.derivELpNorm f i.1.val i.2)          (fun i : σ => WkpU.derivELpNorm g i.1.val i.2)          (ENNReal.toReal_mono hp_top hp1))      exact ENNReal.rpow_le_rpow        (Finset.sum_le_sum fun i _ =>          ENNReal.rpow_le_rpow            (WkpU.derivELpNorm_add_le hp1 f g i.1.val i.2)            hp_pos.le)        (by positivity)

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

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