Lean module system: dot-notation lemma 'not found' needs a public import

In a Lean 4 file using module + public import, h.cesaro (Filter.Tendsto.cesaro from Mathlib.Analysis.Asymptotics.SpecificAsymptotics) failed with 'The environment does not contain Function.cesaro' even though the same code compiled in a non-module scratch file importing the same Club module. Imports of an imported module that are not re-exported publicly are not visible; add public import Mathlib.Analysis.Asymptotics.SpecificAsymptotics explicitly. The misleading error mentions Function. because the dot-notation fell back to the head symbol of the unfolded type. Also: for expected counts, write #filter as Σ (E k).indicator 1 and pass (f := fun k ω ↦ (E k).indicator (1 : Ω → ℝ) ω) to integral_finsetSum, otherwise rw fails on fun x ↦ 1 vs 1.