Maps with equal integrals against all test functions on an open planar set agree almost everywhere

Proved

JHolomorphic.ae_eq_of_forall_integral_smul_eq

by Mazecto · Oct 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

sobolev-spacesweak-derivatives

Let $U\subseteq\mathbb{C}$ be open and let $f,f':\mathbb{C}\to E$ be integrable on every compact subset of $U$ . If $\int\varphi f=\int\varphi f'$ for every real $C^\infty$ function $\varphi$ with compact support in $U$ , then $f=f'$ almost everywhere on $U$ .

Formalization Note $E$ is a finite-dimensional real normed space; almost everywhere on $U$ is ∀ᵐ z ∂(volume.restrict U).

Preamble

import Definitions.Def_JHolomorphic_Setting
import Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff
import Mathlib.Analysis.Calculus.FDeriv.Symmetric
import Mathlib.Analysis.Calculus.FDeriv.Mul
import Mathlib.Analysis.Calculus.ContDiff.Operations
import Mathlib.Analysis.Calculus.ContDiff.Comp

Formal statement

namespace JHolomorphic

open MeasureTheory Filter Topology
open scoped ContDiff

/-- Two maps that are integrable on every compact subset of an open set `U` and have the same
integrals against every real `C^∞` function with compact support in `U` agree almost everywhere
on `U`. -/
theorem ae_eq_of_forall_integral_smul_eq {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    [FiniteDimensional ℝ E] {U : Set ℂ} (hU : IsOpen U) {f f' : ℂ → E}
    (hf : ∀ K ⊆ U, IsCompact K → IntegrableOn f K)
    (hf' : ∀ K ⊆ U, IsCompact K → IntegrableOn f' K)
    (hφ : ∀ φ : ℂ → ℝ, ContDiff ℝ ∞ φ → HasCompactSupport φ → tsupport φ ⊆ U →
      ∫ z, φ z • f z = ∫ z, φ z • f' z) :
    ∀ᵐ z ∂(volume.restrict U), f z = f' z := by
  sorry

end JHolomorphic

Source

Standard (weak derivatives and distribution theory).

View graph