Constancy of distributions with vanishing derivatives

Let Ω be a connected nonempty open subset of a finite-dimensional real normed space E and let μ be an additive Haar measure on E. A Banach-valued distribution on Ω all of whose directional derivatives vanish is integration against a unique constant with respect to μ. No order-zero or finite-mass assumption is made. Conversely, integration against a constant has vanishing derivatives, so this characterizes the constant distributions. The corresponding statement for finite-dimensional vector-valued tests identifies a functional annihilating all derivatives of tests with integration against one fixed continuous linear map; with tests valued in alternating forms, this is the coordinate form of the constancy theorem for currents. The hypothesis quantifies over all directions; by linearity of v ↦ ∂_v T it amounts to the vanishing of the coordinate derivatives along any basis. On the real line, TauCeti.Analysis.Distribution.Constancy.Line states the result for the derivative ∂_1; its local statement has an elementary proof by primitives.

The proof is by regularization. On a ball B(x, r) with B(x, 2r) ⊆ Ω, let ρ be a normalized bump of radius at most r. Since the derivatives of T vanish, its regularization y ↦ T (ρ (· - y)) is constant on B(x, r) (Distribution.translatePairing_eq_of_lineDerivOp_eq_zero), and pairing it with a test φ supported in B(x, r) gives T (ρ ⋆ φ) (Distribution.apply_eq_integral_smul_translatePairing). Hence T (ρ ⋆ φ) = (∫ φ) • T (ρ ⋆ χ) for a test χ of integral one. As the radius of ρ tends to zero, the mollifications converge in the test-function topology (TestFunction.tendsto_mollify), so T φ = (∫ φ) • T χ. These local constants glue on the connected domain (Distribution.existsUnique_eq_ofFun_const_of_locally).

Main declarations

• Distribution.existsUnique_eq_ofFun_const_of_forall_lineDerivOp_eq_zero: a distribution with vanishing derivatives on a connected nonempty open set is integration against a unique constant.
• Distribution.lineDerivOp_ofFun_const: integration against a constant has vanishing derivatives; Distribution.forall_lineDerivOp_eq_zero_iff is the resulting characterization.
• Distribution.existsUnique_sub_eq_ofFun_const_of_forall_lineDerivOp_eq: two distributions with the same derivatives differ by integration against a unique constant.
• TestFunction.existsUnique_eq_integralAgainstBilinCLM_of_forall_lineDeriv_eq_zero: the version for functionals on finite-dimensional vector-valued tests.

References

• L. Hörmander, The Analysis of Linear Partial Differential Operators I, §3.1 (distributions with vanishing derivatives) and §4.1 (regularization).

theorem Distribution.existsUnique_eq_ofFun_const_of_forall_lineDerivOp_eq_zero {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {Ω : TopologicalSpace.Opens E} (T : Distribution Ω F ⊤) (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (hΩ : IsConnected ↑Ω) (hT : ∀ (v : E), LineDeriv.lineDerivOp v T = 0) : ∃! c : F, T = ofFun Ω (fun (x : E) => c) μ ⊤

Constancy of distributions. A Banach-valued distribution on a connected nonempty open subset of a finite-dimensional real normed space whose directional derivatives all vanish is integration against a unique constant, for any additive Haar measure μ.

@[simp]

theorem Distribution.lineDerivOp_ofFun_const {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {Ω : TopologicalSpace.Opens E} (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (c : F) (v : E) : LineDeriv.lineDerivOp v (ofFun Ω (fun (x : E) => c) μ ⊤) = 0

Integration against a constant has vanishing directional derivatives.

theorem Distribution.forall_lineDerivOp_eq_zero_iff {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {Ω : TopologicalSpace.Opens E} (T : Distribution Ω F ⊤) (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (hΩ : IsConnected ↑Ω) : (∀ (v : E), LineDeriv.lineDerivOp v T = 0) ↔ ∃! c : F, T = ofFun Ω (fun (x : E) => c) μ ⊤

On a connected nonempty open domain, vanishing of all directional derivatives characterizes the distributions given by integration against a constant, which is then unique.

theorem Distribution.existsUnique_sub_eq_ofFun_const_of_forall_lineDerivOp_eq {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {Ω : TopologicalSpace.Opens E} (T S : Distribution Ω F ⊤) (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (hΩ : IsConnected ↑Ω) (hTS : ∀ (v : E), LineDeriv.lineDerivOp v T = LineDeriv.lineDerivOp v S) : ∃! c : F, T - S = ofFun Ω (fun (x : E) => c) μ ⊤

Two distributions with the same directional derivatives on a connected nonempty open domain differ by integration against a unique constant.

theorem TestFunction.existsUnique_eq_integralAgainstBilinCLM_of_forall_lineDeriv_eq_zero {E : Type u_1} {F : Type u_2} {V : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V] {Ω : TopologicalSpace.Opens E} (T : CompactConvergenceCLM (RingHom.id ℝ) (TestFunction Ω F ⊤) V) (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (hΩ : IsConnected ↑Ω) (hT : ∀ (v : E) (φ : TestFunction Ω F ⊤), T (LineDeriv.lineDerivOp v φ) = 0) : ∃! A : F →L[ℝ] V, T = (ContinuousLinearMap.toUniformConvergenceCLM (RingHom.id ℝ) V {S : Set (TestFunction Ω F ⊤) | IsCompact S}) (integralAgainstBilinCLM (ContinuousLinearMap.apply ℝ V) μ fun (x : E) => A)

A functional on finite-dimensional vector-valued tests on a connected nonempty open domain that annihilates all their directional derivatives is integration against a unique fixed linear map, for any additive Haar measure μ.