Plain-language statement
The IBP identity passes to the limit.
Exact Lean statement
lemma WkpU.ibp_tendsto [Fact (1 ≤ p)]
{fₙ : ℕ → WkpU d k p U hU}
(g : Lp ℝ p (μU d U))
(hg : Tendsto (fun n => WkpU.toLp (fₙ n)) atTop (𝓝 g))
(n : ℕ+) (hn : n ≤ k) (s : Fin n → Fin d)
(g_ns : Lp ℝ p (μU d U))
(hg_ns : Tendsto (fun j => WkpU.derivtoLp (fₙ j) n hn s) atTop (𝓝 g_ns))
(ψ : (Fin d → ℝ) → ℝ) (hψ : ψ ∈ Cc_inftyU d U) :
∫ x, (g : (Fin d → ℝ) → ℝ) x • (iteratedFDeriv ℝ n ψ x) (unitSeq s) ∂ μU d U =
(-1 : ℝ)^(n : ℕ) • ∫ x, ψ x • (g_ns : (Fin d → ℝ) → ℝ) x ∂ μU d UFormal artifact
Lean source
lemma WkpU.ibp_tendsto [Fact (1 ≤ p)] {fₙ : ℕ → WkpU d k p U hU} (g : Lp ℝ p (μU d U)) (hg : Tendsto (fun n => WkpU.toLp (fₙ n)) atTop (𝓝 g)) (n : ℕ+) (hn : n ≤ k) (s : Fin n → Fin d) (g_ns : Lp ℝ p (μU d U)) (hg_ns : Tendsto (fun j => WkpU.derivtoLp (fₙ j) n hn s) atTop (𝓝 g_ns)) (ψ : (Fin d → ℝ) → ℝ) (hψ : ψ ∈ Cc_inftyU d U) : ∫ x, (g : (Fin d → ℝ) → ℝ) x • (iteratedFDeriv ℝ n ψ x) (unitSeq s) ∂ μU d U = (-1 : ℝ)^(n : ℕ) • ∫ x, ψ x • (g_ns : (Fin d → ℝ) → ℝ) x ∂ μU d U := by have hconv := (Lp.tendsto_Lp_iff_tendsto_eLpNorm' _ g).mp hg have hconv_ns := (Lp.tendsto_Lp_iff_tendsto_eLpNorm' _ g_ns).mp hg_ns have hibp_j : ∀ j, ∫ x, (fₙ j : (Fin d → ℝ) → ℝ) x • (iteratedFDeriv ℝ n ψ x) (unitSeq s) ∂ μU d U = (-1 : ℝ)^(n : ℕ) • ∫ x, ψ x • (WkpU.derivtoLp (fₙ j) n hn s : (Fin d → ℝ) → ℝ) x ∂ μU d U := fun j => by rw [WeakmultiderivU_spec U (fₙ j).val s (WkpU.hasWeakDeriv (fₙ j) n hn s) ψ hψ] congr 1; apply integral_congr_ae filter_upwards [(WkpU.weakDeriv_memLp (fₙ j) n hn s).coeFn_toLp] with x hx simp only [WkpU.derivtoLp, WkpU.weakDeriv] at hx ⊢; rw [hx] have hlhs : Tendsto (fun j => ∫ x, (fₙ j : (Fin d → ℝ) → ℝ) x • (iteratedFDeriv ℝ n ψ x) (unitSeq s) ∂ μU d U) atTop (𝓝 (∫ x, (g : (Fin d → ℝ) → ℝ) x • (iteratedFDeriv ℝ n ψ x) (unitSeq s) ∂ μU d U)) := by have h := integral_tendsto_of_Lploc_tendsto Fact.out (fun j => Lp.memLp (WkpU.toLp (fₙ j))) (Lp.memLp g) (FderivCcinfty s hψ) hconv simp_rw [← smul_eq_mul] at h have hae : ∀ j, (WkpU.toLp (fₙ j) : (Fin d → ℝ) → ℝ) =ᵐ[μU d U] (fₙ j : (Fin d → ℝ) → ℝ) := fun j => (WkpU.memLp (fₙ j)).coeFn_toLp exact h.congr fun j => integral_congr_ae ((hae j).mono fun x hx => by simp [hx]) have hrhs : Tendsto (fun j => (-1 : ℝ)^(n : ℕ) • ∫ x, ψ x • (WkpU.derivtoLp (fₙ j) n hn s : (Fin d → ℝ) → ℝ) x ∂ μU d U) atTop (𝓝 ((-1 : ℝ)^(n : ℕ) • ∫ x, ψ x • (g_ns : (Fin d → ℝ) → ℝ) x ∂ μU d U)) := by apply Filter.Tendsto.const_smul have h := integral_tendsto_of_Lploc_tendsto Fact.out (fun j => Lp.memLp (WkpU.derivtoLp (fₙ j) n hn s)) (Lp.memLp g_ns) hψ hconv_ns simp_rw [smul_eq_mul, mul_comm] at h ⊢ exact h exact (tendsto_nhds_unique (hrhs.congr fun j => (hibp_j j).symm) hlhs).symm- Project
- PDE
- License
- Apache-2.0
- Commit
- 0ab5d79a0d7a
- Source
- PDE/SobolevSpace/SobolevSpaces.lean:803-847
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.