ae_eq_zero_of_forall_dual — Mathlib

English

In the setting with a base field 𝕜, if all dual pairings with f vanish a.e., then f is zero a.e. (general duality principle).

Русский

В базовом поле 𝕜, если все дуальные проекции на f равны нулю почти повсюду, то f = 0 почти повсюду.

LaTeX

$$$\forall c \in \mathrm{StrongDual}(𝕜,E), ⟪f, c⟫ = 0 \ ae \Rightarrow f = 0 \ ae.$$$

Lean4

theorem ae_eq_zero_of_forall_dual [NormedAddCommGroup E] [NormedSpace 𝕜 E] [SecondCountableTopology E] {f : α → E}
    (hf : ∀ c : StrongDual 𝕜 E, (fun x => ⟪f x, c⟫) =ᵐ[μ] 0) : f =ᵐ[μ] 0 :=
  ae_eq_zero_of_forall_dual_of_isSeparable 𝕜 (.of_separableSpace Set.univ) hf
    (Eventually.of_forall fun _ => Set.mem_univ _)

Похожие утверждения