MarkerOccurrence.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem337.pronic line 10
theorem OAI.Problem337.pronic_strictMono line 12
theorem OAI.Problem337.pronic_pos line 17
theorem OAI.Problem337.reciprocal_pronic line 21
theorem OAI.Problem337.sum_reciprocal_pronic line 29
def OAI.Problem337.pronicSet line 38
theorem OAI.Problem337.pronicSet_pos line 41
theorem OAI.Problem337.pronicSet_sum line 45
theorem OAI.Problem337.pronic_succ_not_pronic line 56
theorem OAI.Problem337.insert_pronicSet_one line 67
theorem OAI.Problem337.insert_pronicSet_card line 79
theorem OAI.Problem337.exists_finset_one_with_marker_bounded line 88
Source documentation
Every integer at least two occurs in a finite distinct unit fraction expansion of one. The construction telescopes consecutive reciprocal differences.
```
theorem exists_finset_one_with_marker_bounded (m : ℕ) (hm : 2 ≤ m) :
    ∃ s : Finset ℕ, (∀ d ∈ s, 1 ≤ d) ∧ m ∈ s ∧
      (∑ d ∈ s, (1 : ℚ) / d) = 1 ∧ s.card ≤ m + 1 := by
…
```

theorem OAI.Problem337.exists_finset_one_with_marker line 114

Source documentation

The finite-set version of exact-marker occurrence.

theorem exists_finset_one_with_marker (m : ℕ) (hm : 2 ≤ m) :
    ∃ s : Finset ℕ, (∀ d ∈ s, 1 ≤ d) ∧ m ∈ s ∧
      (∑ d ∈ s, (1 : ℚ) / d) = 1 := by
…

theorem OAI.Problem337.every_exact_marker_occurs_bounded line 121
Source documentation
The telescoping construction uses at most one more term than the marker.
```
theorem every_exact_marker_occurs_bounded (m : ℕ) (hm : 2 ≤ m) :
    ∃ k : ℕ, k ≤ m + 1 ∧ m ∈ D k := by
…
```
Mentions: OAI.Problem337.D
theorem OAI.Problem337.every_exact_marker_occurs_proof line 129
Source documentation
Unconditional exact-marker occurrence, in the qualified expansion model.
```
theorem every_exact_marker_occurs_proof :
    ∀ m : ℕ, 2 ≤ m → ∃ k : ℕ, m ∈ D k := by
…
```
Mentions: OAI.Problem337.D