Distributional derivatives

TheoremThe full derivative of a distribution#●ready to prove

Let \(E\) be a real normed space, \(\Omega \subseteq E\) an open set and \(F\) a real topological vector space, and let \(\mathcal{D}'(\Omega, F)\) be the space of \(F\)-valued distributions on \(\Omega\) (continuous linear maps from the real-valued test functions on \(\Omega\) to \(F\)), with the topology of uniform convergence on compact sets of test functions. For \(v \in E\) and \(T \in \mathcal{D}'(\Omega, F)\), let \(\partial_v T\) be the directional derivative \(\varphi \mapsto -T(\partial_v \varphi)\). Then there is a continuous linear map \(D\) from \(\mathcal{D}'(\Omega, F)\) to the space of continuous linear maps \(E \to \mathcal{D}'(\Omega, F)\) (with the topology of uniform convergence on bounded sets) such that \(D(T)(v) = \partial_v T\) for every \(T \in \mathcal{D}'(\Omega, F)\) and every \(v \in E\).

public theorem_wanted exists_fderiv_distribution
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : Opens E}
    {F : Type*} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F]
    [IsTopologicalAddGroup F] [ContinuousSMul ℝ F] :
    ∃ D : 𝓓'(Ω, F) →L[ℝ] (E →L[ℝ] 𝓓'(Ω, F)), ∀ T v, D T v = ∂_{v} T

Sources

• L. Schwartz, Théorie des distributions, Ch. II.

TheoremA function with vanishing weak third derivative on \((0,1)\) is a.e. a polynomial of degree at most \(2\) on \((0,1)\)#●ready to prove

A function with vanishing weak third derivative on \((0,1)\) is a.e. a polynomial of degree at most \(2\) on \([0,1]\). Let \(f:\mathbb{R}\to\mathbb{R}\) be integrable on \([0,1]\), and suppose that \(\int_{0}^{1} f(x)\,g'''(x)\,dx=0\) for every smooth function \(g:\mathbb{R}\to\mathbb{R}\) whose support is contained in some closed interval \([s,t] \subseteq (0,1)\). Then there are real numbers \(a\), \(b\), \(c\) such that \(f(x)=a+bx+cx^2\) for almost every \(x\in[0,1]\).

public theorem_wanted ae_eq_quadratic_of_integral_mul_iteratedDeriv_three_eq_zero
  (f : ℝ → ℝ)
  (hf : MeasureTheory.MemLp f 1 (MeasureTheory.Measure.restrict MeasureTheory.volume (Set.Icc 0 1)))
  (hweak : ∀ g : ℝ → ℝ, ContDiff ℝ (⊤ : ℕ∞) g →
    (∃ a b : ℝ, Function.support g ⊆ Set.Icc a b ∧
      Set.Icc a b ⊆ Set.Ioo (0 : ℝ) 1) →
      ∫ x in Set.Icc 0 1, f x * deriv (deriv (deriv g)) x = 0) :
  ∃ a b c : ℝ, ∀ᵐ x ∂(MeasureTheory.Measure.restrict MeasureTheory.volume (Set.Icc 0 1)),
    f x = a + b * x + c * x ^ 2

Sources

• MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level II (Functional analysis; Distributions, generalized functions, distribution spaces), problem ma_proofbench_l2_66.

2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.