Project-declaredLean 4.30.0 · mathlib@c5ea00351c28

Wkp U e Norm smul

WkpU.eNorm_smul

partial differential equations Sobolev spaces analysis sobolev spaces

Plain-language statement

Absolute homogeneity for eNorm .

Exact Lean statement

lemma WkpU.eNorm_smul {d : ℕ+} {k : ℕ}{p : ℝ≥0∞}
    {U : Set (Fin d → ℝ)} {hU : IsOpen U}
    (hp1 : p ≥ 1)
    (c : ℝ) (f : WkpU d k p U hU) :
    WkpU.eNorm k p (c • f) = ‖c‖ₑ * WkpU.eNorm k p f

Formal artifact

Lean source

Canonical source

Full Lean sourceLean 4

lemma WkpU.eNorm_smul {d : ℕ+} {k : ℕ}{p : ℝ≥0∞}    {U : Set (Fin d → ℝ)} {hU : IsOpen U}    (hp1 : p ≥ 1)    (c : ℝ) (f : WkpU d k p U hU) :    WkpU.eNorm k p (c • f) = ‖c‖ₑ * WkpU.eNorm k p f := by  simp only [WkpU.eNorm]  split_ifs with hp  · simp_rw [WkpU.derivELpNorm_smul c f]    rw [ENNReal.mul_iSup]    refine iSup_congr fun n => ?_    rw [ENNReal.mul_iSup]  · have hp_pos : 0 < p.toReal :=      ENNReal.toReal_pos       (ne_of_gt (lt_of_lt_of_le zero_lt_one hp1)) hp    simp_rw [WkpU.derivELpNorm_smul c f,             ENNReal.mul_rpow_of_nonneg _ _ hp_pos.le,             ← Finset.mul_sum]    rw [ENNReal.mul_rpow_of_nonneg _ _ (by positivity : (0:ℝ) ≤ 1 / p.toReal),        ← ENNReal.rpow_mul, mul_one_div, div_self hp_pos.ne', ENNReal.rpow_one]

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

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