-- Mathlib/NumberTheory/Padics/MahlerBasis.lean
/--
Second step in Bojanić's proof of Mahler's theorem (equation (11) of [bojanic74]): show that values
`Δ_[1]^[n + p ^ t] f 0` for large enough `n` are bounded by the max of `(‖f‖ / p ^ s)` and `1 / p`
times a sup over values for smaller `n`.

We use `nnnorm`s on the RHS since `Finset.sup` requires an order with a bottom element.
-/
private lemma bojanic_mahler_step2 {f : C(ℤ_[p], E)} {s t : ℕ}
    (hst : ∀ x y : ℤ_[p], ‖x - y‖ ≤ p ^ (-t : ℤ) → ‖f x - f y‖ ≤ ‖f‖ / p ^ s) (n : ℕ) :
    ‖Δ_[1]^[n + p ^ t] f 0‖ ≤ max ↑((Finset.range (p ^ t - 1)).sup
      fun j ↦ ‖Δ_[1]^[n + (j + 1)] f 0‖₊ / p) (‖f‖ / p ^ s)

Proof state:
case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℚ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
s t : ℕ
hst : ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s
n i : ℕ
hi : i < p ^ t - 1
⊢ ‖(p ^ t).choose (i + 1) • Δ_[1]^[n + (i + 1)] (⇑f) 0‖₊ ≤ ‖Δ_[1]^[n + (i + 1)] (⇑f) 0‖₊ / ↑p

Tactic:
rw [← Nat.cast_smul_eq_nsmul ℚ_[p], nnnorm_smul, div_eq_inv_mul]

Result:
case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℚ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
s t : ℕ
hst : ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s
n i : ℕ
hi : i < p ^ t - 1
⊢ ‖↑((p ^ t).choose (i + 1))‖₊ * ‖Δ_[1]^[n + (i + 1)] (⇑f) 0‖₊ ≤ (↑p)⁻¹ * ‖Δ_[1]^[n + (i + 1)] (⇑f) 0‖₊

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℚ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
s t : ℕ
hst : ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s
n i : ℕ
hi : i < p ^ t - 1
this : 0 < (p ^ t).choose (i + 1)
⊢ i + 1 ≠ 0

Tactic:
omega

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℚ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
s t : ℕ
hst : ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s
n i : ℕ
hi : i < p ^ t - 1
⊢ 0 ≤ ‖Δ_[1]^[n + (i + 1)] (⇑f) 0‖₊

Tactic:
simp only [zero_le]

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℚ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
s t : ℕ
hst : ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s
n i : ℕ
hi : i < p ^ t - 1
⊢ i + 1 ≤ p ^ t

Tactic:
omega

Result:
no goals

Proof state:
case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℚ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
s t : ℕ
hst : ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s
n i : ℕ
hi : i < p ^ t - 1
⊢ ‖↑((p ^ t).choose (i + 1))‖₊ * ‖Δ_[1]^[n + (i + 1)] (⇑f) 0‖₊ ≤ (↑p)⁻¹ * ‖Δ_[1]^[n + (i + 1)] (⇑f) 0‖₊

Tactic:
refine mul_le_mul_of_nonneg_right ?_ (by simp only [zero_le])

Result:
case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℚ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
s t : ℕ
hst : ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s
n i : ℕ
hi : i < p ^ t - 1
⊢ ‖↑((p ^ t).choose (i + 1))‖₊ ≤ (↑p)⁻¹

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℚ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
s t : ℕ
hst : ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s
n i : ℕ
x✝ : i ∈ range (n + 1)
⊢ ‖↑((-1) ^ (n - i) * ↑(n.choose i))‖ * ‖f (↑i + ↑(p ^ t)) - f ↑i‖ ≤ ‖f (↑i + ↑(p ^ t)) - f ↑i‖

Tactic:
apply mul_le_of_le_one_left (norm_nonneg _)

Result:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℚ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
s t : ℕ
hst : ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s
n i : ℕ
x✝ : i ∈ range (n + 1)
⊢ ‖↑((-1) ^ (n - i) * ↑(n.choose i))‖ ≤ 1

Proof state:
case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℚ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
s t : ℕ
hst : ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s
n : ℕ
⊢ ‖∑ j ∈ range (p ^ t - 1), (p ^ t).choose (j + 1) • Δ_[1]^[n + (j + 1)] (⇑f) 0‖₊ ≤
    (range (p ^ t - 1)).sup fun j => ‖Δ_[1]^[n + (j + 1)] (⇑f) 0‖₊ / ↑p

Tactic:
refine nnnorm_sum_le_of_forall_le (fun i hi ↦ Finset.le_sup_of_le hi ?_)

Result:
case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℚ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
s t : ℕ
hst : ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s
n i : ℕ
hi : i ∈ range (p ^ t - 1)
⊢ ‖(p ^ t).choose (i + 1) • Δ_[1]^[n + (i + 1)] (⇑f) 0‖₊ ≤ ‖Δ_[1]^[n + (i + 1)] (⇑f) 0‖₊ / ↑p

Proof state:
case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℚ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
s t : ℕ
hst : ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s
n i : ℕ
hi : i < p ^ t - 1
⊢ ‖↑((p ^ t).choose (i + 1))‖₊ ≤ (↑p)⁻¹

Tactic:
have : 0 < (p ^ t).choose (i + 1) := Nat.choose_pos (by omega)

Result:
case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℚ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
s t : ℕ
hst : ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s
n i : ℕ
hi : i < p ^ t - 1
this : 0 < (p ^ t).choose (i + 1)
⊢ ‖↑((p ^ t).choose (i + 1))‖₊ ≤ (↑p)⁻¹

Proof state:
case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℚ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
s t : ℕ
hst : ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s
n i : ℕ
hi : i < p ^ t - 1
this : 0 < (p ^ t).choose (i + 1)
⊢ ‖↑((p ^ t).choose (i + 1))‖₊ ≤ (↑p)⁻¹

Tactic:
rw [← zpow_neg_one, ← coe_le_coe, coe_nnnorm, Padic.norm_eq_zpow_neg_valuation
  (mod_cast this.ne'), coe_zpow, NNReal.coe_natCast,
  zpow_le_zpow_iff_right₀ (mod_cast hp.out.one_lt), neg_le_neg_iff, Padic.valuation_natCast,
  Nat.one_le_cast]

Result:
case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℚ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
s t : ℕ
hst : ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s
n i : ℕ
hi : i < p ^ t - 1
this : 0 < (p ^ t).choose (i + 1)
⊢ 1 ≤ padicValNat p ((p ^ t).choose (i + 1))

Proof state:
case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℚ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
s t : ℕ
hst : ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s
n i : ℕ
hi : i ∈ range (p ^ t - 1)
⊢ ‖(p ^ t).choose (i + 1) • Δ_[1]^[n + (i + 1)] (⇑f) 0‖₊ ≤ ‖Δ_[1]^[n + (i + 1)] (⇑f) 0‖₊ / ↑p

Tactic:
rw [mem_range] at hi

Result:
case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℚ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
s t : ℕ
hst : ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s
n i : ℕ
hi : i < p ^ t - 1
⊢ ‖(p ^ t).choose (i + 1) • Δ_[1]^[n + (i + 1)] (⇑f) 0‖₊ ≤ ‖Δ_[1]^[n + (i + 1)] (⇑f) 0‖₊ / ↑p

Proof state:
case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℚ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
s t : ℕ
hst : ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s
n i : ℕ
hi : i < p ^ t - 1
this : 0 < (p ^ t).choose (i + 1)
⊢ 1 ≤ padicValNat p ((p ^ t).choose (i + 1))

Tactic:
exact one_le_padicValNat_of_dvd this <| hp.out.dvd_choose_pow (by omega) (by omega)

Result:
no goals