English
If the target E is a normed space and t is a separable subset of E in the strong dual pairing sense, and all dual pairings with f vanish almost everywhere, then f is identically zero almost everywhere.
Русский
Если пространства известно, что двойственный модуль является сепарабельным и все сопряженные линейные функционалы дают нулевой результат почти повсюду, тогда функция f равна нулю почти повсюду.
LaTeX
$$$\text{If } t \text{ is separable and } ∀ c\in \mathrm{StrongDual}(𝕜,E), ⟪f, c⟫ = 0\ ae, \text{ then } f = 0 \ ae.$$$
Lean4
theorem ae_eq_zero_of_forall_inner [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [SecondCountableTopology E]
{f : α → E} (hf : ∀ c : E, (fun x => ⟪c, f x⟫_𝕜) =ᵐ[μ] 0) : f =ᵐ[μ] 0 :=
by
let s := denseSeq E
have hs : DenseRange s := denseRange_denseSeq E
have hf' : ∀ᵐ x ∂μ, ∀ n : ℕ, ⟪s n, f x⟫_𝕜 = 0 := ae_all_iff.mpr fun n => hf (s n)
refine hf'.mono fun x hx => ?_
rw [Pi.zero_apply, ← @inner_self_eq_zero 𝕜]
have h_closed : IsClosed {c : E | ⟪c, f x⟫_𝕜 = 0} :=
isClosed_eq (continuous_id.inner continuous_const) continuous_const
exact @isClosed_property ℕ E _ s (fun c => ⟪c, f x⟫_𝕜 = 0) hs h_closed hx _
