English
The p_def is the same as the fixed point solution of the inverse of the sum map.
Русский
P_def эквивалентен фиксированной точке обратной карты суммы.
LaTeX
$$$\text{p_def} = (p \mapsto \sum_{i} a_i b_i^p)^{-1}(1)$$$
Lean4
theorem eventually_atTop_sumTransform_ge :
∃ c > 0, ∀ᶠ (n : ℕ) in atTop, ∀ i, c * g n ≤ sumTransform (p a b) g (r i n) n :=
by
obtain ⟨c₁, hc₁_mem, hc₁⟩ := R.exists_eventually_const_mul_le_r
obtain ⟨c₂, hc₂_mem, hc₂⟩ := R.g_grows_poly.eventually_atTop_ge_nat hc₁_mem
obtain ⟨c₃, hc₃_mem, hc₃⟩ := R.exists_eventually_r_le_const_mul
have hc₁_pos : 0 < c₁ := hc₁_mem.1
have hc₃' : 0 < (1 - c₃) := by have := hc₃_mem.2; linarith
refine ⟨min (c₂ * (1 - c₃)) ((1 - c₃) * c₂ / c₁ ^ ((p a b) + 1)), by positivity, ?_⟩
filter_upwards [hc₁, hc₂, hc₃, R.eventually_r_pos, R.eventually_r_lt_n, eventually_gt_atTop 0] with n hn₁ hn₂ hn₃
hrpos hr_lt_n hn_pos
intro i
have hrpos_i := hrpos i
have g_nonneg : 0 ≤ g n := R.g_nonneg n (by positivity)
cases le_or_gt 0 (p a b + 1) with
| inl hp => -- 0 ≤ (p a b) + 1
calc
sumTransform (p a b) g (r i n) n
_ = n ^ (p a b) * (∑ u ∈ Finset.Ico (r i n) n, g u / u ^ ((p a b) + 1)) := rfl
_ ≥ n ^ (p a b) * (∑ u ∈ Finset.Ico (r i n) n, c₂ * g n / u ^ ((p a b) + 1)) :=
by
gcongr with u hu
rw [Finset.mem_Ico] at hu
have hu' : u ∈ Set.Icc (r i n) n := ⟨hu.1, by cutsat⟩
refine hn₂ u ?_
rw [Set.mem_Icc]
refine ⟨?_, by norm_cast; cutsat⟩
calc
c₁ * n ≤ r i n := by exact hn₁ i
_ ≤ u := by exact_mod_cast hu'.1
_ ≥ n ^ (p a b) * (∑ _u ∈ Finset.Ico (r i n) n, c₂ * g n / n ^ ((p a b) + 1)) :=
by
gcongr with u hu
· rw [Finset.mem_Ico] at hu
have :=
calc
0 < r i n := hrpos_i
_ ≤ u := hu.1
positivity
· rw [Finset.mem_Ico] at hu
exact le_of_lt hu.2
_ ≥ n ^ p a b * #(Ico (r i n) n) • (c₂ * g n / n ^ (p a b + 1)) := by gcongr;
exact Finset.card_nsmul_le_sum _ _ _ (fun x _ => by rfl)
_ = n ^ p a b * #(Ico (r i n) n) * (c₂ * g n / n ^ (p a b + 1)) := by rw [nsmul_eq_mul, mul_assoc]
_ = n ^ (p a b) * (n - r i n) * (c₂ * g n / n ^ ((p a b) + 1)) := by congr;
rw [Nat.card_Ico, Nat.cast_sub (le_of_lt <| hr_lt_n i)]
_ ≥ n ^ (p a b) * (n - c₃ * n) * (c₂ * g n / n ^ ((p a b) + 1)) := by gcongr; exact hn₃ i
_ = n ^ (p a b) * n * (1 - c₃) * (c₂ * g n / n ^ ((p a b) + 1)) := by ring
_ = c₂ * (1 - c₃) * g n * (n ^ ((p a b) + 1) / n ^ ((p a b) + 1)) := by
rw [← Real.rpow_add_one (by positivity) (p a b)]; ring
_ = c₂ * (1 - c₃) * g n := by rw [div_self (by positivity), mul_one]
_ ≥ min (c₂ * (1 - c₃)) ((1 - c₃) * c₂ / c₁ ^ ((p a b) + 1)) * g n := by gcongr; exact min_le_left _ _
| inr hp => -- (p a b) + 1 < 0
calc
sumTransform (p a b) g (r i n) n = n ^ (p a b) * (∑ u ∈ Finset.Ico (r i n) n, g u / u ^ ((p a b) + 1)) := by rfl
_ ≥ n ^ (p a b) * (∑ u ∈ Finset.Ico (r i n) n, c₂ * g n / u ^ ((p a b) + 1)) :=
by
gcongr with u hu
rw [Finset.mem_Ico] at hu
have hu' : u ∈ Set.Icc (r i n) n := ⟨hu.1, by cutsat⟩
refine hn₂ u ?_
rw [Set.mem_Icc]
refine ⟨?_, by norm_cast; cutsat⟩
calc
c₁ * n ≤ r i n := by exact hn₁ i
_ ≤ u := by exact_mod_cast hu'.1
_ ≥ n ^ (p a b) * (∑ _u ∈ Finset.Ico (r i n) n, c₂ * g n / (r i n) ^ ((p a b) + 1)) :=
by
gcongr n ^ (p a b) * (Finset.Ico (r i n) n).sum (fun _ => c₂ * g n / ?_) with u hu
· rw [Finset.mem_Ico] at hu
have :=
calc
0 < r i n := hrpos_i
_ ≤ u := hu.1
positivity
· rw [Finset.mem_Ico] at hu
exact rpow_le_rpow_of_exponent_nonpos (by positivity) (by exact_mod_cast hu.1) (le_of_lt hp)
_ ≥ n ^ p a b * #(Ico (r i n) n) • (c₂ * g n / r i n ^ (p a b + 1)) := by gcongr;
exact Finset.card_nsmul_le_sum _ _ _ (fun x _ => by rfl)
_ = n ^ p a b * #(Ico (r i n) n) * (c₂ * g n / r i n ^ (p a b + 1)) := by rw [nsmul_eq_mul, mul_assoc]
_ ≥ n ^ p a b * #(Ico (r i n) n) * (c₂ * g n / (c₁ * n) ^ (p a b + 1)) :=
by
gcongr n ^ p a b * #(Ico (r i n) n) * (c₂ * g n / ?_)
exact rpow_le_rpow_of_exponent_nonpos (by positivity) (hn₁ i) (le_of_lt hp)
_ = n ^ (p a b) * (n - r i n) * (c₂ * g n / (c₁ * n) ^ ((p a b) + 1)) := by congr;
rw [Nat.card_Ico, Nat.cast_sub (le_of_lt <| hr_lt_n i)]
_ ≥ n ^ (p a b) * (n - c₃ * n) * (c₂ * g n / (c₁ * n) ^ ((p a b) + 1)) := by gcongr; exact hn₃ i
_ = n ^ (p a b) * n * (1 - c₃) * (c₂ * g n / (c₁ * n) ^ ((p a b) + 1)) := by ring
_ = n ^ (p a b) * n * (1 - c₃) * (c₂ * g n / (c₁ ^ ((p a b) + 1) * n ^ ((p a b) + 1))) := by
rw [Real.mul_rpow (by positivity) (by positivity)]
_ = (n ^ ((p a b) + 1) / n ^ ((p a b) + 1)) * (1 - c₃) * c₂ * g n / c₁ ^ ((p a b) + 1) := by
rw [← Real.rpow_add_one (by positivity) (p a b)]; ring
_ = (1 - c₃) * c₂ / c₁ ^ ((p a b) + 1) * g n := by rw [div_self (by positivity), one_mul]; ring
_ ≥ min (c₂ * (1 - c₃)) ((1 - c₃) * c₂ / c₁ ^ ((p a b) + 1)) * g n := by gcongr; exact min_le_right _ _
