Project-declaredLean 4.30.0 · mathlib@c5ea00351c28

Wkp U limit mem

WkpU.limit_mem

partial differential equations Sobolev spaces analysis sobolev spaces

Plain-language statement

Given an Lp limit g and derivative limits g_ns, package them into a WkpU element.

Exact Lean statement

lemma WkpU.limit_mem [Fact (1 ≤ p)]
    (g : Lp ℝ p (μU d U))
    (g_ns : ∀ (n : ℕ+), n ≤ k → (Fin n → Fin d) → Lp ℝ p (μU d U))
    (hid : ∀ (n : ℕ+) (hn : n ≤ k) (s : Fin n → Fin d),
      ∀ ψ ∈ Cc_inftyU d U,
        ∫ x, (g : (Fin d → ℝ) → ℝ) x • (iteratedFDeriv ℝ n ψ x) (unitSeq s) ∂ μU d U =
        (-1 : ℝ)^(n : ℕ) • ∫ x, ψ x •
          (g_ns n hn s : (Fin d → ℝ) → ℝ) x ∂ μU d U) :
    (⟨g, Lp.mem_Lp_locU g⟩ : Lp_locU d 1 U) ∈ (WkpU d k p U hU : Submodule ℝ _)

Formal artifact

Lean source

Canonical source

Full Lean sourceLean 4

lemma WkpU.limit_mem [Fact (1 ≤ p)]    (g : Lp ℝ p (μU d U))    (g_ns : ∀ (n : ℕ+), n ≤ k → (Fin n → Fin d) → Lp ℝ p (μU d U))    (hid : ∀ (n : ℕ+) (hn : n ≤ k) (s : Fin n → Fin d),      ∀ ψ ∈ Cc_inftyU d U,        ∫ x, (g : (Fin d → ℝ) → ℝ) x • (iteratedFDeriv ℝ n ψ x) (unitSeq s) ∂ μU d U =        (-1 : ℝ)^(n : ℕ) • ∫ x, ψ x •          (g_ns n hn s : (Fin d → ℝ) → ℝ) x ∂ μU d U) :    (⟨g, Lp.mem_Lp_locU g⟩ : Lp_locU d 1 U) ∈ (WkpU d k p U hU : Submodule ℝ _) := by  refine ⟨Lp.memLp g, fun n hn s => ?_⟩  have hg_ns_loc : (g_ns n hn s : (Fin d → ℝ) →ₘ[μU d U] ℝ) ∈ Lp_locU d 1 U :=    Lp.mem_Lp_locU (g_ns n hn s)  let g_ns_loc : Lp_locU d 1 U := ⟨g_ns n hn s, hg_ns_loc⟩  let hhas : HasWeakMultiDerivU U ⟨g, Lp.mem_Lp_locU g⟩ s := ⟨g_ns_loc, hid n hn s⟩  exact ⟨hhas, (memLp_congr_ae    (WeakmultiderivU_unique hU s _ hhas g_ns_loc (hid n hn s))).mpr    (Lp.memLp (g_ns n hn s))⟩

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

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