1197.lean`

1 declarations, 1 contain sorry, 0 declared as axioms

References:

erdosproblems.com/1197
[Er80] Erdős, Paul, A survey of problems in combinatorial number theory. Ann. Discrete Math. (1980), 89-115.
[BuMa99] Buczolich, Zoltán and Mauldin, R. Daniel, On the convergence of $\sum^\infty_{n=1}f(nx)$ for measurable functions. Mathematika (1999), 337--341.

Imports (1)

theorem Erdos1197.erdos_1197 sorry line 61 source
depends on sorry what this means
Statement uses: Iff, False, Set, Real, MeasurableSet, LE.le, Set.Ioi, OfNat.ofNat, LT.lt, ENNReal, MeasureTheory.Measure, MeasureTheory.MeasureSpace.volume, Filter.Eventually, Nat, Exists, And, Membership.mem, HSMul.hSMul, HMul.hMul, Filter.atTop and 2 more
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
50 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.