108private theorem CE_factor (m p : ℕ) : 109 ∃ ρ : ℕ → ℕ, StrictMono ρ ∧ (∀ k, k ≤ ρ k) ∧ 110 ∀ k, CE f c R hf (m + p) k = CE f c R hf m (ρ k) := by
proof body
Tactic-mode proof.
111 induction p with 112 | zero => exact ⟨id, strictMono_id, fun k => le_refl k, fun _ => rfl⟩ 113 | succ q ih => 114 obtain ⟨ρ, hρ_mono, hρ_ge, hρ_eq⟩ := ih 115 refine ⟨ρ ∘ LE f c R hf (m + q), 116 hρ_mono.comp (LE_strictMono f c R hf (m + q)), 117 fun k => le_trans (strictMono_id_le (LE_strictMono f c R hf (m + q)) k) 118 (hρ_ge (LE f c R hf (m + q) k)), 119 fun k => ?_⟩ 120 show CE f c R hf (m + (q + 1)) k = CE f c R hf m ((ρ ∘ LE f c R hf (m + q)) k) 121 have h1 : m + (q + 1) = (m + q) + 1 := by omega 122 rw [h1, CE_succ] 123 simp only [Function.comp_apply] 124 exact hρ_eq _ 125
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.