Constancy of distributions on the real line

A Banach-valued distribution on a connected nonempty open subset of the real line has zero first derivative exactly when it is integration against a unique constant. No order-zero or finite-mass assumption is needed. The local statement computes the constant using any integral-one test in a bounded interval: subtracting that test times the integral leaves a mean-zero test, which has a compactly supported smooth primitive in the same interval; this needs no completeness of F. For a Banach space F, the global statements are the case E = ℝ, μ = volume of Distribution.existsUnique_eq_ofFun_const_of_forall_lineDerivOp_eq_zero and Distribution.lineDerivOp_ofFun_const, since ∂_{v} T = v • ∂_{1} T on the line.

The corresponding theorem for finite-dimensional vector-valued tests identifies a functional annihilating derivatives with integration against one fixed continuous linear map. This is the coordinate form of constancy for one-dimensional currents and of uniqueness of distributional primitives up to a constant.

References

• L. Hörmander, The Analysis of Linear Partial Differential Operators I, §2.3, distributions with vanishing derivatives.

theorem Distribution.apply_eq_integral_smul_of_lineDerivOp_eq_zero {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens ℝ} {T : Distribution Ω F ⊤} (hT : LineDeriv.lineDerivOp 1 T = 0) {a b : ℝ} (hab : Set.Ioo a b ⊆ ↑Ω) (η : TestFunction Ω ℝ ⊤) (hη : tsupport ⇑η ⊆ Set.Ioo a b) (hηint : ∫ (x : ℝ), η x = 1) (φ : TestFunction Ω ℝ ⊤) (hφ : tsupport ⇑φ ⊆ Set.Ioo a b) : T φ = (∫ (x : ℝ), φ x) • T η

On a bounded interval, a distribution with zero derivative evaluates a test by its integral and its value on any integral-one test supported in that interval.

theorem Distribution.existsUnique_eq_ofFun_const_of_lineDerivOp_eq_zero {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens ℝ} [CompleteSpace F] (T : Distribution Ω F ⊤) (hΩ : IsConnected ↑Ω) (hT : LineDeriv.lineDerivOp 1 T = 0) : ∃! c : F, T = ofFun Ω (fun (x : ℝ) => c) MeasureTheory.volume ⊤

A distribution on a connected nonempty open subset of the real line with vanishing first derivative is integration against a unique constant.

theorem Distribution.lineDerivOp_one_eq_zero_iff {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens ℝ} [CompleteSpace F] (T : Distribution Ω F ⊤) (hΩ : IsConnected ↑Ω) : LineDeriv.lineDerivOp 1 T = 0 ↔ ∃! c : F, T = ofFun Ω (fun (x : ℝ) => c) MeasureTheory.volume ⊤

On a connected nonempty real open domain, zero derivative characterizes constant Banach-valued distributions. The nonemptiness makes the constant unique.

theorem Distribution.existsUnique_sub_eq_ofFun_const_of_lineDerivOp_eq {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens ℝ} [CompleteSpace F] (T S : Distribution Ω F ⊤) (hΩ : IsConnected ↑Ω) (hTS : LineDeriv.lineDerivOp 1 T = LineDeriv.lineDerivOp 1 S) : ∃! c : F, T - S = ofFun Ω (fun (x : ℝ) => c) MeasureTheory.volume ⊤

Two distributional primitives on a connected nonempty real open domain differ by integration against a unique constant.

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

A functional on finite-dimensional vector-valued tests on a connected nonempty real open domain that annihilates their derivatives is integration against a unique fixed linear map.