[GOAL]
M : Type u_1
inst✝ : OrderedAddCommMonoid M
f : ℕ → M
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
n : ℕ
⊢ ∑ k in Ico 1 (2 ^ n), f k ≤ ∑ k in range n, 2 ^ k • f (2 ^ k)
[PROOFSTEP]
induction' n with n ihn
[GOAL]
case zero
M : Type u_1
inst✝ : OrderedAddCommMonoid M
f : ℕ → M
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
⊢ ∑ k in Ico 1 (2 ^ Nat.zero), f k ≤ ∑ k in range Nat.zero, 2 ^ k • f (2 ^ k)
[PROOFSTEP]
simp
[GOAL]
case succ
M : Type u_1
inst✝ : OrderedAddCommMonoid M
f : ℕ → M
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
n : ℕ
ihn : ∑ k in Ico 1 (2 ^ n), f k ≤ ∑ k in range n, 2 ^ k • f (2 ^ k)
⊢ ∑ k in Ico 1 (2 ^ Nat.succ n), f k ≤ ∑ k in range (Nat.succ n), 2 ^ k • f (2 ^ k)
[PROOFSTEP]
suffices (∑ k in Ico (2 ^ n) (2 ^ (n + 1)), f k) ≤ 2 ^ n • f (2 ^ n)
  by
  rw [sum_range_succ, ← sum_Ico_consecutive]
  exact add_le_add ihn this
  exacts [n.one_le_two_pow, Nat.pow_le_pow_of_le_right zero_lt_two n.le_succ]
[GOAL]
M : Type u_1
inst✝ : OrderedAddCommMonoid M
f : ℕ → M
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
n : ℕ
ihn : ∑ k in Ico 1 (2 ^ n), f k ≤ ∑ k in range n, 2 ^ k • f (2 ^ k)
this : ∑ k in Ico (2 ^ n) (2 ^ (n + 1)), f k ≤ 2 ^ n • f (2 ^ n)
⊢ ∑ k in Ico 1 (2 ^ Nat.succ n), f k ≤ ∑ k in range (Nat.succ n), 2 ^ k • f (2 ^ k)
[PROOFSTEP]
rw [sum_range_succ, ← sum_Ico_consecutive]
[GOAL]
M : Type u_1
inst✝ : OrderedAddCommMonoid M
f : ℕ → M
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
n : ℕ
ihn : ∑ k in Ico 1 (2 ^ n), f k ≤ ∑ k in range n, 2 ^ k • f (2 ^ k)
this : ∑ k in Ico (2 ^ n) (2 ^ (n + 1)), f k ≤ 2 ^ n • f (2 ^ n)
⊢ ∑ i in Ico 1 ?n, f i + ∑ i in Ico ?n (2 ^ Nat.succ n), f i ≤ ∑ x in range n, 2 ^ x • f (2 ^ x) + 2 ^ n • f (2 ^ n)
case n
M : Type u_1
inst✝ : OrderedAddCommMonoid M
f : ℕ → M
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
n : ℕ
ihn : ∑ k in Ico 1 (2 ^ n), f k ≤ ∑ k in range n, 2 ^ k • f (2 ^ k)
this : ∑ k in Ico (2 ^ n) (2 ^ (n + 1)), f k ≤ 2 ^ n • f (2 ^ n)
⊢ ℕ
case hmn
M : Type u_1
inst✝ : OrderedAddCommMonoid M
f : ℕ → M
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
n : ℕ
ihn : ∑ k in Ico 1 (2 ^ n), f k ≤ ∑ k in range n, 2 ^ k • f (2 ^ k)
this : ∑ k in Ico (2 ^ n) (2 ^ (n + 1)), f k ≤ 2 ^ n • f (2 ^ n)
⊢ 1 ≤ ?n
case hnk
M : Type u_1
inst✝ : OrderedAddCommMonoid M
f : ℕ → M
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
n : ℕ
ihn : ∑ k in Ico 1 (2 ^ n), f k ≤ ∑ k in range n, 2 ^ k • f (2 ^ k)
this : ∑ k in Ico (2 ^ n) (2 ^ (n + 1)), f k ≤ 2 ^ n • f (2 ^ n)
⊢ ?n ≤ 2 ^ Nat.succ n
[PROOFSTEP]
exact add_le_add ihn this
[GOAL]
case hmn
M : Type u_1
inst✝ : OrderedAddCommMonoid M
f : ℕ → M
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
n : ℕ
ihn : ∑ k in Ico 1 (2 ^ n), f k ≤ ∑ k in range n, 2 ^ k • f (2 ^ k)
this : ∑ k in Ico (2 ^ n) (2 ^ (n + 1)), f k ≤ 2 ^ n • f (2 ^ n)
⊢ 1 ≤ 2 ^ n
case hnk
M : Type u_1
inst✝ : OrderedAddCommMonoid M
f : ℕ → M
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
n : ℕ
ihn : ∑ k in Ico 1 (2 ^ n), f k ≤ ∑ k in range n, 2 ^ k • f (2 ^ k)
this : ∑ k in Ico (2 ^ n) (2 ^ (n + 1)), f k ≤ 2 ^ n • f (2 ^ n)
⊢ 2 ^ n ≤ 2 ^ Nat.succ n
[PROOFSTEP]
exacts [n.one_le_two_pow, Nat.pow_le_pow_of_le_right zero_lt_two n.le_succ]
[GOAL]
case succ
M : Type u_1
inst✝ : OrderedAddCommMonoid M
f : ℕ → M
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
n : ℕ
ihn : ∑ k in Ico 1 (2 ^ n), f k ≤ ∑ k in range n, 2 ^ k • f (2 ^ k)
⊢ ∑ k in Ico (2 ^ n) (2 ^ (n + 1)), f k ≤ 2 ^ n • f (2 ^ n)
[PROOFSTEP]
have : ∀ k ∈ Ico (2 ^ n) (2 ^ (n + 1)), f k ≤ f (2 ^ n) := fun k hk => hf (pow_pos zero_lt_two _) (mem_Ico.mp hk).1
[GOAL]
case succ
M : Type u_1
inst✝ : OrderedAddCommMonoid M
f : ℕ → M
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
n : ℕ
ihn : ∑ k in Ico 1 (2 ^ n), f k ≤ ∑ k in range n, 2 ^ k • f (2 ^ k)
this : ∀ (k : ℕ), k ∈ Ico (2 ^ n) (2 ^ (n + 1)) → f k ≤ f (2 ^ n)
⊢ ∑ k in Ico (2 ^ n) (2 ^ (n + 1)), f k ≤ 2 ^ n • f (2 ^ n)
[PROOFSTEP]
convert sum_le_sum this
[GOAL]
case h.e'_4
M : Type u_1
inst✝ : OrderedAddCommMonoid M
f : ℕ → M
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
n : ℕ
ihn : ∑ k in Ico 1 (2 ^ n), f k ≤ ∑ k in range n, 2 ^ k • f (2 ^ k)
this : ∀ (k : ℕ), k ∈ Ico (2 ^ n) (2 ^ (n + 1)) → f k ≤ f (2 ^ n)
⊢ 2 ^ n • f (2 ^ n) = ∑ i in Ico (2 ^ n) (2 ^ (n + 1)), f (2 ^ n)
[PROOFSTEP]
simp [pow_succ, two_mul]
[GOAL]
M : Type u_1
inst✝ : OrderedAddCommMonoid M
f : ℕ → M
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
n : ℕ
⊢ ∑ k in range (2 ^ n), f k ≤ f 0 + ∑ k in range n, 2 ^ k • f (2 ^ k)
[PROOFSTEP]
convert add_le_add_left (le_sum_condensed' hf n) (f 0)
[GOAL]
case h.e'_3
M : Type u_1
inst✝ : OrderedAddCommMonoid M
f : ℕ → M
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
n : ℕ
⊢ ∑ k in range (2 ^ n), f k = f 0 + ∑ k in Ico 1 (2 ^ n), f k
[PROOFSTEP]
rw [← sum_range_add_sum_Ico _ n.one_le_two_pow, sum_range_succ, sum_range_zero, zero_add]
[GOAL]
M : Type u_1
inst✝ : OrderedAddCommMonoid M
f : ℕ → M
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
n : ℕ
⊢ ∑ k in range n, 2 ^ k • f (2 ^ (k + 1)) ≤ ∑ k in Ico 2 (2 ^ n + 1), f k
[PROOFSTEP]
induction' n with n ihn
[GOAL]
case zero
M : Type u_1
inst✝ : OrderedAddCommMonoid M
f : ℕ → M
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
⊢ ∑ k in range Nat.zero, 2 ^ k • f (2 ^ (k + 1)) ≤ ∑ k in Ico 2 (2 ^ Nat.zero + 1), f k
[PROOFSTEP]
simp
[GOAL]
case succ
M : Type u_1
inst✝ : OrderedAddCommMonoid M
f : ℕ → M
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
n : ℕ
ihn : ∑ k in range n, 2 ^ k • f (2 ^ (k + 1)) ≤ ∑ k in Ico 2 (2 ^ n + 1), f k
⊢ ∑ k in range (Nat.succ n), 2 ^ k • f (2 ^ (k + 1)) ≤ ∑ k in Ico 2 (2 ^ Nat.succ n + 1), f k
[PROOFSTEP]
suffices 2 ^ n • f (2 ^ (n + 1)) ≤ ∑ k in Ico (2 ^ n + 1) (2 ^ (n + 1) + 1), f k
  by
  rw [sum_range_succ, ← sum_Ico_consecutive]
  exacts [add_le_add ihn this, (add_le_add_right n.one_le_two_pow _ : 1 + 1 ≤ 2 ^ n + 1),
    add_le_add_right (Nat.pow_le_pow_of_le_right zero_lt_two n.le_succ) _]
[GOAL]
M : Type u_1
inst✝ : OrderedAddCommMonoid M
f : ℕ → M
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
n : ℕ
ihn : ∑ k in range n, 2 ^ k • f (2 ^ (k + 1)) ≤ ∑ k in Ico 2 (2 ^ n + 1), f k
this : 2 ^ n • f (2 ^ (n + 1)) ≤ ∑ k in Ico (2 ^ n + 1) (2 ^ (n + 1) + 1), f k
⊢ ∑ k in range (Nat.succ n), 2 ^ k • f (2 ^ (k + 1)) ≤ ∑ k in Ico 2 (2 ^ Nat.succ n + 1), f k
[PROOFSTEP]
rw [sum_range_succ, ← sum_Ico_consecutive]
[GOAL]
M : Type u_1
inst✝ : OrderedAddCommMonoid M
f : ℕ → M
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
n : ℕ
ihn : ∑ k in range n, 2 ^ k • f (2 ^ (k + 1)) ≤ ∑ k in Ico 2 (2 ^ n + 1), f k
this : 2 ^ n • f (2 ^ (n + 1)) ≤ ∑ k in Ico (2 ^ n + 1) (2 ^ (n + 1) + 1), f k
⊢ ∑ x in range n, 2 ^ x • f (2 ^ (x + 1)) + 2 ^ n • f (2 ^ (n + 1)) ≤
    ∑ i in Ico 2 ?n, f i + ∑ i in Ico ?n (2 ^ Nat.succ n + 1), f i
case n
M : Type u_1
inst✝ : OrderedAddCommMonoid M
f : ℕ → M
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
n : ℕ
ihn : ∑ k in range n, 2 ^ k • f (2 ^ (k + 1)) ≤ ∑ k in Ico 2 (2 ^ n + 1), f k
this : 2 ^ n • f (2 ^ (n + 1)) ≤ ∑ k in Ico (2 ^ n + 1) (2 ^ (n + 1) + 1), f k
⊢ ℕ
case hmn
M : Type u_1
inst✝ : OrderedAddCommMonoid M
f : ℕ → M
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
n : ℕ
ihn : ∑ k in range n, 2 ^ k • f (2 ^ (k + 1)) ≤ ∑ k in Ico 2 (2 ^ n + 1), f k
this : 2 ^ n • f (2 ^ (n + 1)) ≤ ∑ k in Ico (2 ^ n + 1) (2 ^ (n + 1) + 1), f k
⊢ 2 ≤ ?n
case hnk
M : Type u_1
inst✝ : OrderedAddCommMonoid M
f : ℕ → M
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
n : ℕ
ihn : ∑ k in range n, 2 ^ k • f (2 ^ (k + 1)) ≤ ∑ k in Ico 2 (2 ^ n + 1), f k
this : 2 ^ n • f (2 ^ (n + 1)) ≤ ∑ k in Ico (2 ^ n + 1) (2 ^ (n + 1) + 1), f k
⊢ ?n ≤ 2 ^ Nat.succ n + 1
[PROOFSTEP]
exacts [add_le_add ihn this, (add_le_add_right n.one_le_two_pow _ : 1 + 1 ≤ 2 ^ n + 1),
  add_le_add_right (Nat.pow_le_pow_of_le_right zero_lt_two n.le_succ) _]
[GOAL]
case succ
M : Type u_1
inst✝ : OrderedAddCommMonoid M
f : ℕ → M
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
n : ℕ
ihn : ∑ k in range n, 2 ^ k • f (2 ^ (k + 1)) ≤ ∑ k in Ico 2 (2 ^ n + 1), f k
⊢ 2 ^ n • f (2 ^ (n + 1)) ≤ ∑ k in Ico (2 ^ n + 1) (2 ^ (n + 1) + 1), f k
[PROOFSTEP]
have : ∀ k ∈ Ico (2 ^ n + 1) (2 ^ (n + 1) + 1), f (2 ^ (n + 1)) ≤ f k := fun k hk =>
  hf (n.one_le_two_pow.trans_lt <| (Nat.lt_succ_of_le le_rfl).trans_le (mem_Ico.mp hk).1)
    (Nat.le_of_lt_succ <| (mem_Ico.mp hk).2)
[GOAL]
case succ
M : Type u_1
inst✝ : OrderedAddCommMonoid M
f : ℕ → M
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
n : ℕ
ihn : ∑ k in range n, 2 ^ k • f (2 ^ (k + 1)) ≤ ∑ k in Ico 2 (2 ^ n + 1), f k
this : ∀ (k : ℕ), k ∈ Ico (2 ^ n + 1) (2 ^ (n + 1) + 1) → f (2 ^ (n + 1)) ≤ f k
⊢ 2 ^ n • f (2 ^ (n + 1)) ≤ ∑ k in Ico (2 ^ n + 1) (2 ^ (n + 1) + 1), f k
[PROOFSTEP]
convert sum_le_sum this
[GOAL]
case h.e'_3
M : Type u_1
inst✝ : OrderedAddCommMonoid M
f : ℕ → M
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
n : ℕ
ihn : ∑ k in range n, 2 ^ k • f (2 ^ (k + 1)) ≤ ∑ k in Ico 2 (2 ^ n + 1), f k
this : ∀ (k : ℕ), k ∈ Ico (2 ^ n + 1) (2 ^ (n + 1) + 1) → f (2 ^ (n + 1)) ≤ f k
⊢ 2 ^ n • f (2 ^ (n + 1)) = ∑ i in Ico (2 ^ n + 1) (2 ^ (n + 1) + 1), f (2 ^ (n + 1))
[PROOFSTEP]
simp [pow_succ, two_mul]
[GOAL]
M : Type u_1
inst✝ : OrderedAddCommMonoid M
f : ℕ → M
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
n : ℕ
⊢ ∑ k in range (n + 1), 2 ^ k • f (2 ^ k) ≤ f 1 + 2 • ∑ k in Ico 2 (2 ^ n + 1), f k
[PROOFSTEP]
convert add_le_add_left (nsmul_le_nsmul_of_le_right (sum_condensed_le' hf n) 2) (f 1)
[GOAL]
case h.e'_3
M : Type u_1
inst✝ : OrderedAddCommMonoid M
f : ℕ → M
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
n : ℕ
⊢ ∑ k in range (n + 1), 2 ^ k • f (2 ^ k) = f 1 + 2 • ∑ k in range n, 2 ^ k • f (2 ^ (k + 1))
[PROOFSTEP]
simp [sum_range_succ', add_comm, pow_succ, mul_nsmul', sum_nsmul]
[GOAL]
f : ℕ → ℝ≥0∞
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
⊢ ∑' (k : ℕ), f k ≤ f 0 + ∑' (k : ℕ), ↑(2 ^ k) * f (2 ^ k)
[PROOFSTEP]
rw [ENNReal.tsum_eq_iSup_nat' (Nat.tendsto_pow_atTop_atTop_of_one_lt _root_.one_lt_two)]
[GOAL]
f : ℕ → ℝ≥0∞
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
⊢ ⨆ (i : ℕ), ∑ a in Finset.range (2 ^ i), f a ≤ f 0 + ∑' (k : ℕ), ↑(2 ^ k) * f (2 ^ k)
[PROOFSTEP]
refine' iSup_le fun n => (Finset.le_sum_condensed hf n).trans (add_le_add_left _ _)
[GOAL]
f : ℕ → ℝ≥0∞
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
n : ℕ
⊢ ∑ k in Finset.range n, 2 ^ k • f (2 ^ k) ≤ ∑' (k : ℕ), ↑(2 ^ k) * f (2 ^ k)
[PROOFSTEP]
simp only [nsmul_eq_mul, Nat.cast_pow, Nat.cast_two]
[GOAL]
f : ℕ → ℝ≥0∞
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
n : ℕ
⊢ ∑ x in Finset.range n, 2 ^ x * f (2 ^ x) ≤ ∑' (k : ℕ), 2 ^ k * f (2 ^ k)
[PROOFSTEP]
apply ENNReal.sum_le_tsum
[GOAL]
f : ℕ → ℝ≥0∞
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
⊢ ∑' (k : ℕ), ↑(2 ^ k) * f (2 ^ k) ≤ f 1 + 2 * ∑' (k : ℕ), f k
[PROOFSTEP]
rw [ENNReal.tsum_eq_iSup_nat' (tendsto_atTop_mono Nat.le_succ tendsto_id), two_mul, ← two_nsmul]
[GOAL]
f : ℕ → ℝ≥0∞
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
⊢ ⨆ (i : ℕ), ∑ a in Finset.range (Nat.succ i), ↑(2 ^ a) * f (2 ^ a) ≤ f 1 + 2 • ∑' (k : ℕ), f k
[PROOFSTEP]
refine'
  iSup_le fun n =>
    le_trans _ (add_le_add_left (nsmul_le_nsmul_of_le_right (ENNReal.sum_le_tsum <| Finset.Ico 2 (2 ^ n + 1)) _) _)
[GOAL]
f : ℕ → ℝ≥0∞
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
n : ℕ
⊢ ∑ a in Finset.range (Nat.succ n), ↑(2 ^ a) * f (2 ^ a) ≤ f 1 + 2 • ∑ x in Finset.Ico 2 (2 ^ n + 1), f x
[PROOFSTEP]
simpa using Finset.sum_condensed_le hf n
[GOAL]
f : ℕ → ℝ≥0
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
⊢ (Summable fun k => 2 ^ k * f (2 ^ k)) ↔ Summable f
[PROOFSTEP]
simp only [← ENNReal.tsum_coe_ne_top_iff_summable, Ne.def, not_iff_not, ENNReal.coe_mul, ENNReal.coe_pow,
  ENNReal.coe_two]
[GOAL]
f : ℕ → ℝ≥0
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
⊢ ∑' (b : ℕ), 2 ^ b * ↑(f (2 ^ b)) = ⊤ ↔ ∑' (b : ℕ), ↑(f b) = ⊤
[PROOFSTEP]
constructor
[GOAL]
case mp
f : ℕ → ℝ≥0
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
⊢ ∑' (b : ℕ), 2 ^ b * ↑(f (2 ^ b)) = ⊤ → ∑' (b : ℕ), ↑(f b) = ⊤
[PROOFSTEP]
intro h
[GOAL]
case mpr
f : ℕ → ℝ≥0
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
⊢ ∑' (b : ℕ), ↑(f b) = ⊤ → ∑' (b : ℕ), 2 ^ b * ↑(f (2 ^ b)) = ⊤
[PROOFSTEP]
intro h
[GOAL]
case mp
f : ℕ → ℝ≥0
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h : ∑' (b : ℕ), 2 ^ b * ↑(f (2 ^ b)) = ⊤
⊢ ∑' (b : ℕ), ↑(f b) = ⊤
[PROOFSTEP]
replace hf : ∀ m n, 1 < m → m ≤ n → (f n : ℝ≥0∞) ≤ f m := fun m n hm hmn =>
  ENNReal.coe_le_coe.2 (hf (zero_lt_one.trans hm) hmn)
[GOAL]
case mp
f : ℕ → ℝ≥0
h : ∑' (b : ℕ), 2 ^ b * ↑(f (2 ^ b)) = ⊤
hf : ∀ (m n : ℕ), 1 < m → m ≤ n → ↑(f n) ≤ ↑(f m)
⊢ ∑' (b : ℕ), ↑(f b) = ⊤
[PROOFSTEP]
simpa [h, ENNReal.add_eq_top, ENNReal.mul_eq_top] using ENNReal.tsum_condensed_le hf
[GOAL]
case mpr
f : ℕ → ℝ≥0
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h : ∑' (b : ℕ), ↑(f b) = ⊤
⊢ ∑' (b : ℕ), 2 ^ b * ↑(f (2 ^ b)) = ⊤
[PROOFSTEP]
replace hf : ∀ m n, 0 < m → m ≤ n → (f n : ℝ≥0∞) ≤ f m := fun m n hm hmn => ENNReal.coe_le_coe.2 (hf hm hmn)
[GOAL]
case mpr
f : ℕ → ℝ≥0
h : ∑' (b : ℕ), ↑(f b) = ⊤
hf : ∀ (m n : ℕ), 0 < m → m ≤ n → ↑(f n) ≤ ↑(f m)
⊢ ∑' (b : ℕ), 2 ^ b * ↑(f (2 ^ b)) = ⊤
[PROOFSTEP]
simpa [h, ENNReal.add_eq_top] using ENNReal.le_tsum_condensed hf
[GOAL]
f : ℕ → ℝ
h_nonneg : ∀ (n : ℕ), 0 ≤ f n
h_mono : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
⊢ (Summable fun k => 2 ^ k * f (2 ^ k)) ↔ Summable f
[PROOFSTEP]
lift f to ℕ → ℝ≥0 using h_nonneg
[GOAL]
case intro
f : ℕ → ℝ≥0
h_mono : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → (fun i => ↑(f i)) n ≤ (fun i => ↑(f i)) m
⊢ (Summable fun k => 2 ^ k * (fun i => ↑(f i)) (2 ^ k)) ↔ Summable fun i => ↑(f i)
[PROOFSTEP]
simp only [NNReal.coe_le_coe] at *
[GOAL]
case intro
f : ℕ → ℝ≥0
h_mono : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
⊢ (Summable fun k => 2 ^ k * ↑(f (2 ^ k))) ↔ Summable fun i => ↑(f i)
[PROOFSTEP]
exact_mod_cast NNReal.summable_condensed_iff h_mono
[GOAL]
p : ℝ
⊢ (Summable fun n => (↑n ^ p)⁻¹) ↔ 1 < p
[PROOFSTEP]
cases' le_or_lt 0 p with hp hp
[GOAL]
case inl
p : ℝ
hp : 0 ≤ p
⊢ (Summable fun n => (↑n ^ p)⁻¹) ↔ 1 < p
[PROOFSTEP]
rw [← summable_condensed_iff_of_nonneg]
[GOAL]
case inl
p : ℝ
hp : 0 ≤ p
⊢ (Summable fun k => 2 ^ k * (↑(2 ^ k) ^ p)⁻¹) ↔ 1 < p
[PROOFSTEP]
simp_rw [Nat.cast_pow, Nat.cast_two, ← rpow_nat_cast, ← rpow_mul zero_lt_two.le, mul_comm _ p, rpow_mul zero_lt_two.le,
  rpow_nat_cast, ← inv_pow, ← mul_pow, summable_geometric_iff_norm_lt_1]
[GOAL]
case inl
p : ℝ
hp : 0 ≤ p
⊢ ‖2 * (2 ^ p)⁻¹‖ < 1 ↔ 1 < p
[PROOFSTEP]
nth_rw 1 [← rpow_one 2]
[GOAL]
case inl
p : ℝ
hp : 0 ≤ p
⊢ ‖2 ^ 1 * (2 ^ p)⁻¹‖ < 1 ↔ 1 < p
[PROOFSTEP]
rw [← division_def, ← rpow_sub zero_lt_two, norm_eq_abs, abs_of_pos (rpow_pos_of_pos zero_lt_two _),
  rpow_lt_one_iff zero_lt_two.le]
[GOAL]
case inl
p : ℝ
hp : 0 ≤ p
⊢ 2 = 0 ∧ 1 - p ≠ 0 ∨ 1 < 2 ∧ 1 - p < 0 ∨ 2 < 1 ∧ 0 < 1 - p ↔ 1 < p
[PROOFSTEP]
norm_num
[GOAL]
case inl.h_nonneg
p : ℝ
hp : 0 ≤ p
⊢ ∀ (n : ℕ), 0 ≤ (↑n ^ p)⁻¹
[PROOFSTEP]
intro n
[GOAL]
case inl.h_nonneg
p : ℝ
hp : 0 ≤ p
n : ℕ
⊢ 0 ≤ (↑n ^ p)⁻¹
[PROOFSTEP]
exact inv_nonneg.2 (rpow_nonneg_of_nonneg n.cast_nonneg _)
[GOAL]
case inl.h_mono
p : ℝ
hp : 0 ≤ p
⊢ ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → (↑n ^ p)⁻¹ ≤ (↑m ^ p)⁻¹
[PROOFSTEP]
intro m n hm hmn
[GOAL]
case inl.h_mono
p : ℝ
hp : 0 ≤ p
m n : ℕ
hm : 0 < m
hmn : m ≤ n
⊢ (↑n ^ p)⁻¹ ≤ (↑m ^ p)⁻¹
[PROOFSTEP]
exact
  inv_le_inv_of_le (rpow_pos_of_pos (Nat.cast_pos.2 hm) _)
    (rpow_le_rpow m.cast_nonneg (Nat.cast_le.2 hmn) hp)
      -- If `p < 0`, then `1 / n ^ p` tends to infinity, thus the series diverges.
[GOAL]
case inr
p : ℝ
hp : p < 0
⊢ (Summable fun n => (↑n ^ p)⁻¹) ↔ 1 < p
[PROOFSTEP]
suffices ¬Summable (fun n => ((n : ℝ) ^ p)⁻¹ : ℕ → ℝ)
  by
  have : ¬1 < p := fun hp₁ => hp.not_le (zero_le_one.trans hp₁.le)
  simpa only [this, iff_false]
[GOAL]
p : ℝ
hp : p < 0
this : ¬Summable fun n => (↑n ^ p)⁻¹
⊢ (Summable fun n => (↑n ^ p)⁻¹) ↔ 1 < p
[PROOFSTEP]
have : ¬1 < p := fun hp₁ => hp.not_le (zero_le_one.trans hp₁.le)
[GOAL]
p : ℝ
hp : p < 0
this✝ : ¬Summable fun n => (↑n ^ p)⁻¹
this : ¬1 < p
⊢ (Summable fun n => (↑n ^ p)⁻¹) ↔ 1 < p
[PROOFSTEP]
simpa only [this, iff_false]
[GOAL]
case inr
p : ℝ
hp : p < 0
⊢ ¬Summable fun n => (↑n ^ p)⁻¹
[PROOFSTEP]
intro h
[GOAL]
case inr
p : ℝ
hp : p < 0
h : Summable fun n => (↑n ^ p)⁻¹
⊢ False
[PROOFSTEP]
obtain ⟨k : ℕ, hk₁ : ((k : ℝ) ^ p)⁻¹ < 1, hk₀ : k ≠ 0⟩ :=
  ((h.tendsto_cofinite_zero.eventually (gt_mem_nhds zero_lt_one)).and (eventually_cofinite_ne 0)).exists
[GOAL]
case inr.intro.intro
p : ℝ
hp : p < 0
h : Summable fun n => (↑n ^ p)⁻¹
k : ℕ
hk₁ : (↑k ^ p)⁻¹ < 1
hk₀ : k ≠ 0
⊢ False
[PROOFSTEP]
apply hk₀
[GOAL]
case inr.intro.intro
p : ℝ
hp : p < 0
h : Summable fun n => (↑n ^ p)⁻¹
k : ℕ
hk₁ : (↑k ^ p)⁻¹ < 1
hk₀ : k ≠ 0
⊢ k = 0
[PROOFSTEP]
rw [← pos_iff_ne_zero, ← @Nat.cast_pos ℝ] at hk₀
[GOAL]
case inr.intro.intro
p : ℝ
hp : p < 0
h : Summable fun n => (↑n ^ p)⁻¹
k : ℕ
hk₁ : (↑k ^ p)⁻¹ < 1
hk₀ : 0 < ↑k
⊢ k = 0
[PROOFSTEP]
simpa [inv_lt_one_iff_of_pos (rpow_pos_of_pos hk₀ _), one_lt_rpow_iff_of_pos hk₀, hp, hp.not_lt, hk₀] using hk₁
[GOAL]
p : ℝ
⊢ (Summable fun n => ↑n ^ p) ↔ p < -1
[PROOFSTEP]
rcases neg_surjective p with ⟨p, rfl⟩
[GOAL]
case intro
p : ℝ
⊢ (Summable fun n => ↑n ^ (-p)) ↔ -p < -1
[PROOFSTEP]
simp [rpow_neg]
[GOAL]
p : ℝ
⊢ (Summable fun n => 1 / ↑n ^ p) ↔ 1 < p
[PROOFSTEP]
simp
[GOAL]
p : ℕ
⊢ (Summable fun n => (↑n ^ p)⁻¹) ↔ 1 < p
[PROOFSTEP]
simp only [← rpow_nat_cast, Real.summable_nat_rpow_inv, Nat.one_lt_cast]
[GOAL]
p : ℕ
⊢ (Summable fun n => 1 / ↑n ^ p) ↔ 1 < p
[PROOFSTEP]
simp only [one_div, Real.summable_nat_pow_inv]
[GOAL]
p : ℕ
⊢ (Summable fun n => 1 / ↑n ^ p) ↔ 1 < p
[PROOFSTEP]
refine'
  ⟨fun h => Real.summable_one_div_nat_pow.mp (h.comp_injective Nat.cast_injective), fun h =>
    summable_int_of_summable_nat (Real.summable_one_div_nat_pow.mpr h)
      (((Real.summable_one_div_nat_pow.mpr h).mul_left <| 1 / (-1 : ℝ) ^ p).congr fun n => _)⟩
[GOAL]
p : ℕ
h : 1 < p
n : ℕ
⊢ 1 / (-1) ^ p * (1 / ↑n ^ p) = 1 / ↑(-↑n) ^ p
[PROOFSTEP]
conv_rhs => rw [Int.cast_neg, neg_eq_neg_one_mul, mul_pow, ← div_div]
[GOAL]
p : ℕ
h : 1 < p
n : ℕ
| 1 / ↑(-↑n) ^ p
[PROOFSTEP]
rw [Int.cast_neg, neg_eq_neg_one_mul, mul_pow, ← div_div]
[GOAL]
p : ℕ
h : 1 < p
n : ℕ
| 1 / ↑(-↑n) ^ p
[PROOFSTEP]
rw [Int.cast_neg, neg_eq_neg_one_mul, mul_pow, ← div_div]
[GOAL]
p : ℕ
h : 1 < p
n : ℕ
| 1 / ↑(-↑n) ^ p
[PROOFSTEP]
rw [Int.cast_neg, neg_eq_neg_one_mul, mul_pow, ← div_div]
[GOAL]
p : ℕ
h : 1 < p
n : ℕ
⊢ 1 / (-1) ^ p * (1 / ↑n ^ p) = 1 / (-1) ^ p / ↑↑n ^ p
[PROOFSTEP]
conv_lhs => rw [mul_div, mul_one]
[GOAL]
p : ℕ
h : 1 < p
n : ℕ
| 1 / (-1) ^ p * (1 / ↑n ^ p)
[PROOFSTEP]
rw [mul_div, mul_one]
[GOAL]
p : ℕ
h : 1 < p
n : ℕ
| 1 / (-1) ^ p * (1 / ↑n ^ p)
[PROOFSTEP]
rw [mul_div, mul_one]
[GOAL]
p : ℕ
h : 1 < p
n : ℕ
| 1 / (-1) ^ p * (1 / ↑n ^ p)
[PROOFSTEP]
rw [mul_div, mul_one]
[GOAL]
b : ℝ
hb : 1 < b
⊢ Summable fun n => |↑n| ^ (-b)
[PROOFSTEP]
apply summable_int_of_summable_nat
[GOAL]
case hp
b : ℝ
hb : 1 < b
⊢ Summable fun n => |↑↑n| ^ (-b)
case hn b : ℝ hb : 1 < b ⊢ Summable fun n => |↑(-↑n)| ^ (-b)
[PROOFSTEP]
on_goal 2 => simp_rw [Int.cast_neg, abs_neg]
[GOAL]
case hp
b : ℝ
hb : 1 < b
⊢ Summable fun n => |↑↑n| ^ (-b)
case hn b : ℝ hb : 1 < b ⊢ Summable fun n => |↑(-↑n)| ^ (-b)
[PROOFSTEP]
on_goal 2 => simp_rw [Int.cast_neg, abs_neg]
[GOAL]
case hn
b : ℝ
hb : 1 < b
⊢ Summable fun n => |↑(-↑n)| ^ (-b)
[PROOFSTEP]
simp_rw [Int.cast_neg, abs_neg]
[GOAL]
case hp
b : ℝ
hb : 1 < b
⊢ Summable fun n => |↑↑n| ^ (-b)
case hn b : ℝ hb : 1 < b ⊢ Summable fun n => |↑↑n| ^ (-b)
[PROOFSTEP]
all_goals
  simp_rw [Int.cast_ofNat, fun n : ℕ => abs_of_nonneg (n.cast_nonneg : 0 ≤ (n : ℝ))]
  rwa [Real.summable_nat_rpow, neg_lt_neg_iff]
[GOAL]
case hp
b : ℝ
hb : 1 < b
⊢ Summable fun n => |↑↑n| ^ (-b)
[PROOFSTEP]
simp_rw [Int.cast_ofNat, fun n : ℕ => abs_of_nonneg (n.cast_nonneg : 0 ≤ (n : ℝ))]
[GOAL]
case hp
b : ℝ
hb : 1 < b
⊢ Summable fun n => ↑n ^ (-b)
[PROOFSTEP]
rwa [Real.summable_nat_rpow, neg_lt_neg_iff]
[GOAL]
case hn
b : ℝ
hb : 1 < b
⊢ Summable fun n => |↑↑n| ^ (-b)
[PROOFSTEP]
simp_rw [Int.cast_ofNat, fun n : ℕ => abs_of_nonneg (n.cast_nonneg : 0 ≤ (n : ℝ))]
[GOAL]
case hn
b : ℝ
hb : 1 < b
⊢ Summable fun n => ↑n ^ (-b)
[PROOFSTEP]
rwa [Real.summable_nat_rpow, neg_lt_neg_iff]
[GOAL]
⊢ ¬Summable fun n => (↑n)⁻¹
[PROOFSTEP]
have : ¬Summable (fun n => ((n : ℝ) ^ 1)⁻¹ : ℕ → ℝ) := mt (Real.summable_nat_pow_inv (p := 1)).1 (lt_irrefl 1)
[GOAL]
this : ¬Summable fun n => (↑n ^ 1)⁻¹
⊢ ¬Summable fun n => (↑n)⁻¹
[PROOFSTEP]
simpa
[GOAL]
⊢ ¬Summable fun n => 1 / ↑n
[PROOFSTEP]
simpa only [inv_eq_one_div] using Real.not_summable_nat_cast_inv
[GOAL]
⊢ Tendsto (fun n => ∑ i in Finset.range n, 1 / (↑i + 1)) atTop atTop
[PROOFSTEP]
rw [← not_summable_iff_tendsto_nat_atTop_of_nonneg]
[GOAL]
⊢ ¬Summable fun i => 1 / (↑i + 1)
[PROOFSTEP]
exact_mod_cast mt (_root_.summable_nat_add_iff 1).1 Real.not_summable_one_div_nat_cast
[GOAL]
⊢ ∀ (n : ℕ), 0 ≤ 1 / (↑n + 1)
[PROOFSTEP]
exact fun i => div_nonneg zero_le_one i.cast_add_one_pos.le
[GOAL]
p : ℝ
⊢ (Summable fun n => (↑n ^ p)⁻¹) ↔ 1 < p
[PROOFSTEP]
simp [← NNReal.summable_coe]
[GOAL]
p : ℝ
⊢ (Summable fun n => ↑n ^ p) ↔ p < -1
[PROOFSTEP]
simp [← NNReal.summable_coe]
[GOAL]
p : ℝ
⊢ (Summable fun n => 1 / ↑n ^ p) ↔ 1 < p
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
k n : ℕ
hk : k ≠ 0
h : k ≤ n
⊢ ∑ i in Ioc k n, (↑i ^ 2)⁻¹ ≤ (↑k)⁻¹ - (↑n)⁻¹
[PROOFSTEP]
refine' Nat.le_induction _ _ n h
[GOAL]
case refine'_1
α : Type u_1
inst✝ : LinearOrderedField α
k n : ℕ
hk : k ≠ 0
h : k ≤ n
⊢ ∑ i in Ioc k k, (↑i ^ 2)⁻¹ ≤ (↑k)⁻¹ - (↑k)⁻¹
[PROOFSTEP]
simp only [Ioc_self, sum_empty, sub_self, le_refl]
[GOAL]
case refine'_2
α : Type u_1
inst✝ : LinearOrderedField α
k n : ℕ
hk : k ≠ 0
h : k ≤ n
⊢ ∀ (n : ℕ),
    k ≤ n → ∑ i in Ioc k n, (↑i ^ 2)⁻¹ ≤ (↑k)⁻¹ - (↑n)⁻¹ → ∑ i in Ioc k (n + 1), (↑i ^ 2)⁻¹ ≤ (↑k)⁻¹ - (↑(n + 1))⁻¹
[PROOFSTEP]
intro n hn IH
[GOAL]
case refine'_2
α : Type u_1
inst✝ : LinearOrderedField α
k n✝ : ℕ
hk : k ≠ 0
h : k ≤ n✝
n : ℕ
hn : k ≤ n
IH : ∑ i in Ioc k n, (↑i ^ 2)⁻¹ ≤ (↑k)⁻¹ - (↑n)⁻¹
⊢ ∑ i in Ioc k (n + 1), (↑i ^ 2)⁻¹ ≤ (↑k)⁻¹ - (↑(n + 1))⁻¹
[PROOFSTEP]
rw [sum_Ioc_succ_top hn]
[GOAL]
case refine'_2
α : Type u_1
inst✝ : LinearOrderedField α
k n✝ : ℕ
hk : k ≠ 0
h : k ≤ n✝
n : ℕ
hn : k ≤ n
IH : ∑ i in Ioc k n, (↑i ^ 2)⁻¹ ≤ (↑k)⁻¹ - (↑n)⁻¹
⊢ ∑ k in Ioc k n, (↑k ^ 2)⁻¹ + (↑(n + 1) ^ 2)⁻¹ ≤ (↑k)⁻¹ - (↑(n + 1))⁻¹
[PROOFSTEP]
apply (add_le_add IH le_rfl).trans
[GOAL]
case refine'_2
α : Type u_1
inst✝ : LinearOrderedField α
k n✝ : ℕ
hk : k ≠ 0
h : k ≤ n✝
n : ℕ
hn : k ≤ n
IH : ∑ i in Ioc k n, (↑i ^ 2)⁻¹ ≤ (↑k)⁻¹ - (↑n)⁻¹
⊢ (↑k)⁻¹ - (↑n)⁻¹ + (↑(n + 1) ^ 2)⁻¹ ≤ (↑k)⁻¹ - (↑(n + 1))⁻¹
[PROOFSTEP]
simp only [sub_eq_add_neg, add_assoc, Nat.cast_add, Nat.cast_one, le_add_neg_iff_add_le, add_le_iff_nonpos_right,
  neg_add_le_iff_le_add, add_zero]
[GOAL]
case refine'_2
α : Type u_1
inst✝ : LinearOrderedField α
k n✝ : ℕ
hk : k ≠ 0
h : k ≤ n✝
n : ℕ
hn : k ≤ n
IH : ∑ i in Ioc k n, (↑i ^ 2)⁻¹ ≤ (↑k)⁻¹ - (↑n)⁻¹
⊢ ((↑n + 1) ^ 2)⁻¹ + (↑n + 1)⁻¹ ≤ (↑n)⁻¹
[PROOFSTEP]
have A : 0 < (n : α) := by simpa using hk.bot_lt.trans_le hn
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
k n✝ : ℕ
hk : k ≠ 0
h : k ≤ n✝
n : ℕ
hn : k ≤ n
IH : ∑ i in Ioc k n, (↑i ^ 2)⁻¹ ≤ (↑k)⁻¹ - (↑n)⁻¹
⊢ 0 < ↑n
[PROOFSTEP]
simpa using hk.bot_lt.trans_le hn
[GOAL]
case refine'_2
α : Type u_1
inst✝ : LinearOrderedField α
k n✝ : ℕ
hk : k ≠ 0
h : k ≤ n✝
n : ℕ
hn : k ≤ n
IH : ∑ i in Ioc k n, (↑i ^ 2)⁻¹ ≤ (↑k)⁻¹ - (↑n)⁻¹
A : 0 < ↑n
⊢ ((↑n + 1) ^ 2)⁻¹ + (↑n + 1)⁻¹ ≤ (↑n)⁻¹
[PROOFSTEP]
have B : 0 < (n : α) + 1 := by linarith
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
k n✝ : ℕ
hk : k ≠ 0
h : k ≤ n✝
n : ℕ
hn : k ≤ n
IH : ∑ i in Ioc k n, (↑i ^ 2)⁻¹ ≤ (↑k)⁻¹ - (↑n)⁻¹
A : 0 < ↑n
⊢ 0 < ↑n + 1
[PROOFSTEP]
linarith
[GOAL]
case refine'_2
α : Type u_1
inst✝ : LinearOrderedField α
k n✝ : ℕ
hk : k ≠ 0
h : k ≤ n✝
n : ℕ
hn : k ≤ n
IH : ∑ i in Ioc k n, (↑i ^ 2)⁻¹ ≤ (↑k)⁻¹ - (↑n)⁻¹
A : 0 < ↑n
B : 0 < ↑n + 1
⊢ ((↑n + 1) ^ 2)⁻¹ + (↑n + 1)⁻¹ ≤ (↑n)⁻¹
[PROOFSTEP]
field_simp [B.ne']
[GOAL]
case refine'_2
α : Type u_1
inst✝ : LinearOrderedField α
k n✝ : ℕ
hk : k ≠ 0
h : k ≤ n✝
n : ℕ
hn : k ≤ n
IH : ∑ i in Ioc k n, (↑i ^ 2)⁻¹ ≤ (↑k)⁻¹ - (↑n)⁻¹
A : 0 < ↑n
B : 0 < ↑n + 1
⊢ (↑n + 1 + (↑n + 1) ^ 2) / ((↑n + 1) ^ 2 * (↑n + 1)) ≤ 1 / ↑n
[PROOFSTEP]
rw [div_le_div_iff _ A, ← sub_nonneg]
[GOAL]
case refine'_2
α : Type u_1
inst✝ : LinearOrderedField α
k n✝ : ℕ
hk : k ≠ 0
h : k ≤ n✝
n : ℕ
hn : k ≤ n
IH : ∑ i in Ioc k n, (↑i ^ 2)⁻¹ ≤ (↑k)⁻¹ - (↑n)⁻¹
A : 0 < ↑n
B : 0 < ↑n + 1
⊢ 0 ≤ 1 * ((↑n + 1) ^ 2 * (↑n + 1)) - (↑n + 1 + (↑n + 1) ^ 2) * ↑n
[PROOFSTEP]
ring_nf
[GOAL]
case refine'_2
α : Type u_1
inst✝ : LinearOrderedField α
k n✝ : ℕ
hk : k ≠ 0
h : k ≤ n✝
n : ℕ
hn : k ≤ n
IH : ∑ i in Ioc k n, (↑i ^ 2)⁻¹ ≤ (↑k)⁻¹ - (↑n)⁻¹
A : 0 < ↑n
B : 0 < ↑n + 1
⊢ 0 ≤ 1 + ↑n
[PROOFSTEP]
rw [add_comm]
[GOAL]
case refine'_2
α : Type u_1
inst✝ : LinearOrderedField α
k n✝ : ℕ
hk : k ≠ 0
h : k ≤ n✝
n : ℕ
hn : k ≤ n
IH : ∑ i in Ioc k n, (↑i ^ 2)⁻¹ ≤ (↑k)⁻¹ - (↑n)⁻¹
A : 0 < ↑n
B : 0 < ↑n + 1
⊢ 0 ≤ ↑n + 1
[PROOFSTEP]
exact B.le
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
k n✝ : ℕ
hk : k ≠ 0
h : k ≤ n✝
n : ℕ
hn : k ≤ n
IH : ∑ i in Ioc k n, (↑i ^ 2)⁻¹ ≤ (↑k)⁻¹ - (↑n)⁻¹
A : 0 < ↑n
B : 0 < ↑n + 1
⊢ 0 < (↑n + 1) ^ 2 * (↑n + 1)
[PROOFSTEP]
positivity
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
k n : ℕ
⊢ ∑ i in Ioo k n, (↑i ^ 2)⁻¹ ≤ ∑ i in Ioc k (max (k + 1) n), (↑i ^ 2)⁻¹
[PROOFSTEP]
apply sum_le_sum_of_subset_of_nonneg
[GOAL]
case h
α : Type u_1
inst✝ : LinearOrderedField α
k n : ℕ
⊢ Ioo k n ⊆ Ioc k (max (k + 1) n)
[PROOFSTEP]
intro x hx
[GOAL]
case h
α : Type u_1
inst✝ : LinearOrderedField α
k n x : ℕ
hx : x ∈ Ioo k n
⊢ x ∈ Ioc k (max (k + 1) n)
[PROOFSTEP]
simp only [mem_Ioo] at hx
[GOAL]
case h
α : Type u_1
inst✝ : LinearOrderedField α
k n x : ℕ
hx : k < x ∧ x < n
⊢ x ∈ Ioc k (max (k + 1) n)
[PROOFSTEP]
simp only [hx, hx.2.le, mem_Ioc, le_max_iff, or_true_iff, and_self_iff]
[GOAL]
case hf
α : Type u_1
inst✝ : LinearOrderedField α
k n : ℕ
⊢ ∀ (i : ℕ), i ∈ Ioc k (max (k + 1) n) → ¬i ∈ Ioo k n → 0 ≤ (↑i ^ 2)⁻¹
[PROOFSTEP]
intro i _hi _hident
[GOAL]
case hf
α : Type u_1
inst✝ : LinearOrderedField α
k n i : ℕ
_hi : i ∈ Ioc k (max (k + 1) n)
_hident : ¬i ∈ Ioo k n
⊢ 0 ≤ (↑i ^ 2)⁻¹
[PROOFSTEP]
positivity
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
k n : ℕ
⊢ ∑ i in Ioc k (max (k + 1) n), (↑i ^ 2)⁻¹ ≤ ((↑k + 1) ^ 2)⁻¹ + ∑ i in Ioc (Nat.succ k) (max (k + 1) n), (↑i ^ 2)⁻¹
[PROOFSTEP]
rw [← Nat.Icc_succ_left, ← Nat.Ico_succ_right, sum_eq_sum_Ico_succ_bot]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
k n : ℕ
⊢ (↑(Nat.succ k) ^ 2)⁻¹ + ∑ k in Ico (Nat.succ k + 1) (Nat.succ (max (k + 1) n)), (↑k ^ 2)⁻¹ ≤
    ((↑k + 1) ^ 2)⁻¹ + ∑ i in Ioc (Nat.succ k) (max (k + 1) n), (↑i ^ 2)⁻¹
case hab α : Type u_1 inst✝ : LinearOrderedField α k n : ℕ ⊢ Nat.succ k < Nat.succ (max (k + 1) n)
[PROOFSTEP]
swap
[GOAL]
case hab
α : Type u_1
inst✝ : LinearOrderedField α
k n : ℕ
⊢ Nat.succ k < Nat.succ (max (k + 1) n)
[PROOFSTEP]
exact Nat.succ_lt_succ ((Nat.lt_succ_self k).trans_le (le_max_left _ _))
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
k n : ℕ
⊢ (↑(Nat.succ k) ^ 2)⁻¹ + ∑ k in Ico (Nat.succ k + 1) (Nat.succ (max (k + 1) n)), (↑k ^ 2)⁻¹ ≤
    ((↑k + 1) ^ 2)⁻¹ + ∑ i in Ioc (Nat.succ k) (max (k + 1) n), (↑i ^ 2)⁻¹
[PROOFSTEP]
rw [Nat.Ico_succ_right, Nat.Icc_succ_left, Nat.cast_succ]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
k n : ℕ
⊢ ((↑k + 1) ^ 2)⁻¹ + ∑ i in Ioc (Nat.succ k) (max (k + 1) n), (↑i ^ 2)⁻¹ ≤ ((↑k + 1) ^ 2)⁻¹ + (↑k + 1)⁻¹
[PROOFSTEP]
refine' add_le_add le_rfl ((sum_Ioc_inv_sq_le_sub _ (le_max_left _ _)).trans _)
[GOAL]
case refine'_1
α : Type u_1
inst✝ : LinearOrderedField α
k n : ℕ
⊢ Nat.succ k ≠ 0
[PROOFSTEP]
simp only [Ne.def, Nat.succ_ne_zero, not_false_iff]
[GOAL]
case refine'_2
α : Type u_1
inst✝ : LinearOrderedField α
k n : ℕ
⊢ (↑(Nat.succ k))⁻¹ - (↑(max (Nat.succ k) n))⁻¹ ≤ (↑k + 1)⁻¹
[PROOFSTEP]
simp only [Nat.cast_succ, one_div, sub_le_self_iff, inv_nonneg, Nat.cast_nonneg]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
k n : ℕ
⊢ ((↑k + 1) ^ 2)⁻¹ + (↑k + 1)⁻¹ ≤ 1 / (↑k + 1) + 1 / (↑k + 1)
[PROOFSTEP]
have A : (1 : α) ≤ k + 1 := by simp only [le_add_iff_nonneg_left, Nat.cast_nonneg]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
k n : ℕ
⊢ 1 ≤ ↑k + 1
[PROOFSTEP]
simp only [le_add_iff_nonneg_left, Nat.cast_nonneg]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
k n : ℕ
A : 1 ≤ ↑k + 1
⊢ ((↑k + 1) ^ 2)⁻¹ + (↑k + 1)⁻¹ ≤ 1 / (↑k + 1) + 1 / (↑k + 1)
[PROOFSTEP]
simp_rw [← one_div]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
k n : ℕ
A : 1 ≤ ↑k + 1
⊢ 1 / (↑k + 1) ^ 2 + 1 / (↑k + 1) ≤ 1 / (↑k + 1) + 1 / (↑k + 1)
[PROOFSTEP]
apply add_le_add_right
[GOAL]
case bc
α : Type u_1
inst✝ : LinearOrderedField α
k n : ℕ
A : 1 ≤ ↑k + 1
⊢ 1 / (↑k + 1) ^ 2 ≤ 1 / (↑k + 1)
[PROOFSTEP]
refine' div_le_div zero_le_one le_rfl (zero_lt_one.trans_le A) _
[GOAL]
case bc
α : Type u_1
inst✝ : LinearOrderedField α
k n : ℕ
A : 1 ≤ ↑k + 1
⊢ ↑k + 1 ≤ (↑k + 1) ^ 2
[PROOFSTEP]
simpa using pow_le_pow A one_le_two
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
k n : ℕ
⊢ 1 / (↑k + 1) + 1 / (↑k + 1) = 2 / (↑k + 1)
[PROOFSTEP]
ring


[GOAL]
R : Type u
Γ₀ : Type v
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x y : R
hx : x ∈ {x | ↑v x ≤ 1}
hy : y ∈ {x | ↑v x ≤ 1}
⊢ x * y ∈ {x | ↑v x ≤ 1}
[PROOFSTEP]
simp only [Set.mem_setOf_eq, _root_.map_mul, mul_le_one' hx hy]
[GOAL]
R : Type u
Γ₀ : Type v
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
⊢ 0 ∈
    {
          toSubsemigroup :=
            { carrier := {x | ↑v x ≤ 1},
              mul_mem' := (_ : ∀ {x y : R}, x ∈ {x | ↑v x ≤ 1} → y ∈ {x | ↑v x ≤ 1} → ↑v (x * y) ≤ 1) },
          one_mem' := (_ : ↑v 1 ≤ 1) }.toSubsemigroup.carrier
[PROOFSTEP]
simp only [Set.mem_setOf_eq, _root_.map_zero, zero_le']
[GOAL]
R : Type u
Γ₀ : Type v
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
hx :
  x ∈
    {
            toSubmonoid :=
              {
                toSubsemigroup :=
                  { carrier := {x | ↑v x ≤ 1},
                    mul_mem' := (_ : ∀ {x y : R}, x ∈ {x | ↑v x ≤ 1} → y ∈ {x | ↑v x ≤ 1} → ↑v (x * y) ≤ 1) },
                one_mem' := (_ : ↑v 1 ≤ 1) },
            add_mem' :=
              (_ :
                ∀ {x y : R},
                  x ∈
                      {
                            toSubsemigroup :=
                              { carrier := {x | ↑v x ≤ 1},
                                mul_mem' :=
                                  (_ : ∀ {x y : R}, x ∈ {x | ↑v x ≤ 1} → y ∈ {x | ↑v x ≤ 1} → ↑v (x * y) ≤ 1) },
                            one_mem' := (_ : ↑v 1 ≤ 1) }.toSubsemigroup.carrier →
                    y ∈
                        {
                              toSubsemigroup :=
                                { carrier := {x | ↑v x ≤ 1},
                                  mul_mem' :=
                                    (_ : ∀ {x y : R}, x ∈ {x | ↑v x ≤ 1} → y ∈ {x | ↑v x ≤ 1} → ↑v (x * y) ≤ 1) },
                              one_mem' := (_ : ↑v 1 ≤ 1) }.toSubsemigroup.carrier →
                      ↑v (x + y) ≤ 1),
            zero_mem' := (_ : ↑v 0 ≤ 1) }.toSubmonoid.toSubsemigroup.carrier
⊢ -x ∈
    {
            toSubmonoid :=
              {
                toSubsemigroup :=
                  { carrier := {x | ↑v x ≤ 1},
                    mul_mem' := (_ : ∀ {x y : R}, x ∈ {x | ↑v x ≤ 1} → y ∈ {x | ↑v x ≤ 1} → ↑v (x * y) ≤ 1) },
                one_mem' := (_ : ↑v 1 ≤ 1) },
            add_mem' :=
              (_ :
                ∀ {x y : R},
                  x ∈
                      {
                            toSubsemigroup :=
                              { carrier := {x | ↑v x ≤ 1},
                                mul_mem' :=
                                  (_ : ∀ {x y : R}, x ∈ {x | ↑v x ≤ 1} → y ∈ {x | ↑v x ≤ 1} → ↑v (x * y) ≤ 1) },
                            one_mem' := (_ : ↑v 1 ≤ 1) }.toSubsemigroup.carrier →
                    y ∈
                        {
                              toSubsemigroup :=
                                { carrier := {x | ↑v x ≤ 1},
                                  mul_mem' :=
                                    (_ : ∀ {x y : R}, x ∈ {x | ↑v x ≤ 1} → y ∈ {x | ↑v x ≤ 1} → ↑v (x * y) ≤ 1) },
                              one_mem' := (_ : ↑v 1 ≤ 1) }.toSubsemigroup.carrier →
                      ↑v (x + y) ≤ 1),
            zero_mem' := (_ : ↑v 0 ≤ 1) }.toSubmonoid.toSubsemigroup.carrier
[PROOFSTEP]
simp only [Set.mem_setOf_eq] at hx
[GOAL]
R : Type u
Γ₀ : Type v
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
hx : ↑v x ≤ 1
⊢ -x ∈
    {
            toSubmonoid :=
              {
                toSubsemigroup :=
                  { carrier := {x | ↑v x ≤ 1},
                    mul_mem' := (_ : ∀ {x y : R}, x ∈ {x | ↑v x ≤ 1} → y ∈ {x | ↑v x ≤ 1} → ↑v (x * y) ≤ 1) },
                one_mem' := (_ : ↑v 1 ≤ 1) },
            add_mem' :=
              (_ :
                ∀ {x y : R},
                  x ∈
                      {
                            toSubsemigroup :=
                              { carrier := {x | ↑v x ≤ 1},
                                mul_mem' :=
                                  (_ : ∀ {x y : R}, x ∈ {x | ↑v x ≤ 1} → y ∈ {x | ↑v x ≤ 1} → ↑v (x * y) ≤ 1) },
                            one_mem' := (_ : ↑v 1 ≤ 1) }.toSubsemigroup.carrier →
                    y ∈
                        {
                              toSubsemigroup :=
                                { carrier := {x | ↑v x ≤ 1},
                                  mul_mem' :=
                                    (_ : ∀ {x y : R}, x ∈ {x | ↑v x ≤ 1} → y ∈ {x | ↑v x ≤ 1} → ↑v (x * y) ≤ 1) },
                              one_mem' := (_ : ↑v 1 ≤ 1) }.toSubsemigroup.carrier →
                      ↑v (x + y) ≤ 1),
            zero_mem' := (_ : ↑v 0 ≤ 1) }.toSubmonoid.toSubsemigroup.carrier
[PROOFSTEP]
simpa only [Set.mem_setOf_eq, map_neg]
[GOAL]
R : Type u
Γ₀ : Type v
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝³ : CommRing O
inst✝² : Algebra O R
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : Integers v O
x : O
hx : IsUnit x
u : Oˣ
hu : ↑u = x
⊢ 1 ≤ ↑v (↑(algebraMap O R) x)
[PROOFSTEP]
rw [← v.map_one, ← (algebraMap O R).map_one, ← u.mul_inv, ← mul_one (v (algebraMap O R x)), hu,
  (algebraMap O R).map_mul, v.map_mul]
[GOAL]
R : Type u
Γ₀ : Type v
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝³ : CommRing O
inst✝² : Algebra O R
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : Integers v O
x : O
hx : IsUnit x
u : Oˣ
hu : ↑u = x
⊢ ↑v (↑(algebraMap O R) x) * ↑v (↑(algebraMap O R) ↑u⁻¹) ≤ ↑v (↑(algebraMap O R) x) * 1
[PROOFSTEP]
exact mul_le_mul_left' (hv.2 (u⁻¹ : Units O)) _
[GOAL]
R : Type u
Γ₀ : Type v
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝³ : CommRing O
inst✝² : Algebra O R
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : Integers v O
x : O
hx : IsUnit (↑(algebraMap O R) x)
hvx : ↑v (↑(algebraMap O R) x) = 1
u : ((fun x => R) x)ˣ
hu : ↑u = ↑(algebraMap O R) x
h1 : ↑v ↑u ≤ 1
⊢ ↑v ↑u⁻¹ ≤ 1
[PROOFSTEP]
rw [← one_mul (v _), ← hvx, ← v.map_mul, ← hu, u.mul_inv, hu, hvx, v.map_one]
[GOAL]
R : Type u
Γ₀ : Type v
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝³ : CommRing O
inst✝² : Algebra O R
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : Integers v O
x : O
hx : IsUnit (↑(algebraMap O R) x)
hvx : ↑v (↑(algebraMap O R) x) = 1
u : ((fun x => R) x)ˣ
hu : ↑u = ↑(algebraMap O R) x
h1 : ↑v ↑u ≤ 1
h2 : ↑v ↑u⁻¹ ≤ 1
r1 : O
hr1 : ↑(algebraMap O R) r1 = ↑u
r2 : O
hr2 : ↑(algebraMap O R) r2 = ↑u⁻¹
⊢ ↑(algebraMap O R) (r1 * r2) = ↑(algebraMap O R) 1
[PROOFSTEP]
rw [RingHom.map_mul, RingHom.map_one, hr1, hr2, Units.mul_inv]
[GOAL]
R : Type u
Γ₀ : Type v
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝³ : CommRing O
inst✝² : Algebra O R
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : Integers v O
x : O
hx : IsUnit (↑(algebraMap O R) x)
hvx : ↑v (↑(algebraMap O R) x) = 1
u : ((fun x => R) x)ˣ
hu : ↑u = ↑(algebraMap O R) x
h1 : ↑v ↑u ≤ 1
h2 : ↑v ↑u⁻¹ ≤ 1
r1 : O
hr1 : ↑(algebraMap O R) r1 = ↑u
r2 : O
hr2 : ↑(algebraMap O R) r2 = ↑u⁻¹
⊢ ↑(algebraMap O R) (r2 * r1) = ↑(algebraMap O R) 1
[PROOFSTEP]
rw [RingHom.map_mul, RingHom.map_one, hr1, hr2, Units.inv_mul]
[GOAL]
R : Type u
Γ₀ : Type v
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝³ : CommRing O
inst✝² : Algebra O R
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : Integers v O
x y : O
h : x ∣ y
⊢ ↑v (↑(algebraMap O R) y) ≤ ↑v (↑(algebraMap O R) x)
[PROOFSTEP]
let ⟨z, hz⟩ := h
[GOAL]
R : Type u
Γ₀ : Type v
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝³ : CommRing O
inst✝² : Algebra O R
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : Integers v O
x y : O
h : x ∣ y
z : O
hz : y = x * z
⊢ ↑v (↑(algebraMap O R) y) ≤ ↑v (↑(algebraMap O R) x)
[PROOFSTEP]
rw [← mul_one (v (algebraMap O R x)), hz, RingHom.map_mul, v.map_mul]
[GOAL]
R : Type u
Γ₀ : Type v
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝³ : CommRing O
inst✝² : Algebra O R
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : Integers v O
x y : O
h : x ∣ y
z : O
hz : y = x * z
⊢ ↑v (↑(algebraMap O R) x) * ↑v (↑(algebraMap O R) z) ≤ ↑v (↑(algebraMap O R) x) * 1
[PROOFSTEP]
exact mul_le_mul_left' (hv.2 z) _
[GOAL]
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : Integers v O
x y : O
h : ↑v (↑(algebraMap O F) x) ≤ ↑v (↑(algebraMap O F) y)
hy : ↑(algebraMap O F) y ≠ 0
⊢ ↑v ((↑(algebraMap O F) y)⁻¹ * ↑(algebraMap O F) x) ≤ 1
[PROOFSTEP]
rw [← v.map_one, ← inv_mul_cancel hy, v.map_mul, v.map_mul]
[GOAL]
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : Integers v O
x y : O
h : ↑v (↑(algebraMap O F) x) ≤ ↑v (↑(algebraMap O F) y)
hy : ↑(algebraMap O F) y ≠ 0
⊢ ↑v (↑(algebraMap O F) y)⁻¹ * ↑v (↑(algebraMap O F) x) ≤ ↑v (↑(algebraMap O F) y)⁻¹ * ↑v (↑(algebraMap O F) y)
[PROOFSTEP]
exact mul_le_mul_left' h _


[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : SMul 𝕜 E
s : Set E
f g : E → β
inst✝ : SemilatticeSup β
hf : QuasiconvexOn 𝕜 s f
hg : QuasiconvexOn 𝕜 s g
⊢ QuasiconvexOn 𝕜 s (f ⊔ g)
[PROOFSTEP]
intro r
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : SMul 𝕜 E
s : Set E
f g : E → β
inst✝ : SemilatticeSup β
hf : QuasiconvexOn 𝕜 s f
hg : QuasiconvexOn 𝕜 s g
r : β
⊢ Convex 𝕜 {x | x ∈ s ∧ (f ⊔ g) x ≤ r}
[PROOFSTEP]
simp_rw [Pi.sup_def, sup_le_iff, Set.sep_and]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : SMul 𝕜 E
s : Set E
f g : E → β
inst✝ : SemilatticeSup β
hf : QuasiconvexOn 𝕜 s f
hg : QuasiconvexOn 𝕜 s g
r : β
⊢ Convex 𝕜 ({x | x ∈ s ∧ f x ≤ r} ∩ {x | x ∈ s ∧ g x ≤ r})
[PROOFSTEP]
exact (hf r).inter (hg r)
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : LinearOrder β
inst✝ : SMul 𝕜 E
s : Set E
f g : E → β
⊢ QuasilinearOn 𝕜 s f ↔
    Convex 𝕜 s ∧
      ∀ ⦃x : E⦄,
        x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f (a • x + b • y) ∈ uIcc (f x) (f y)
[PROOFSTEP]
rw [QuasilinearOn, quasiconvexOn_iff_le_max, quasiconcaveOn_iff_min_le, and_and_and_comm, and_self_iff]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : LinearOrder β
inst✝ : SMul 𝕜 E
s : Set E
f g : E → β
⊢ (Convex 𝕜 s ∧
      (∀ ⦃x : E⦄,
          x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f (a • x + b • y) ≤ max (f x) (f y)) ∧
        ∀ ⦃x : E⦄,
          x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → min (f x) (f y) ≤ f (a • x + b • y)) ↔
    Convex 𝕜 s ∧
      ∀ ⦃x : E⦄,
        x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f (a • x + b • y) ∈ uIcc (f x) (f y)
[PROOFSTEP]
apply and_congr_right'
[GOAL]
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : LinearOrder β
inst✝ : SMul 𝕜 E
s : Set E
f g : E → β
⊢ ((∀ ⦃x : E⦄,
        x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f (a • x + b • y) ≤ max (f x) (f y)) ∧
      ∀ ⦃x : E⦄,
        x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → min (f x) (f y) ≤ f (a • x + b • y)) ↔
    ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f (a • x + b • y) ∈ uIcc (f x) (f y)
[PROOFSTEP]
simp_rw [← forall_and, ← Icc_min_max, mem_Icc, and_comm]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : LinearOrder β
inst✝ : SMul 𝕜 E
s : Set E
f g : E → β
hf : QuasiconvexOn 𝕜 s f
r : β
⊢ Convex 𝕜 {x | x ∈ s ∧ f x < r}
[PROOFSTEP]
refine' fun x hx y hy a b ha hb hab => _
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : LinearOrder β
inst✝ : SMul 𝕜 E
s : Set E
f g : E → β
hf : QuasiconvexOn 𝕜 s f
r : β
x : E
hx : x ∈ {x | x ∈ s ∧ f x < r}
y : E
hy : y ∈ {x | x ∈ s ∧ f x < r}
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ {x | x ∈ s ∧ f x < r}
[PROOFSTEP]
have h := hf _ ⟨hx.1, le_max_left _ _⟩ ⟨hy.1, le_max_right _ _⟩ ha hb hab
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : LinearOrder β
inst✝ : SMul 𝕜 E
s : Set E
f g : E → β
hf : QuasiconvexOn 𝕜 s f
r : β
x : E
hx : x ∈ {x | x ∈ s ∧ f x < r}
y : E
hy : y ∈ {x | x ∈ s ∧ f x < r}
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h : a • x + b • y ∈ {x_1 | x_1 ∈ s ∧ f x_1 ≤ max (f x) (f y)}
⊢ a • x + b • y ∈ {x | x ∈ s ∧ f x < r}
[PROOFSTEP]
exact ⟨h.1, h.2.trans_lt <| max_lt hx.2 hy.2⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝¹ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → β
inst✝ : LinearOrder β
hf : QuasilinearOn 𝕜 s f
⊢ MonotoneOn f s ∨ AntitoneOn f s
[PROOFSTEP]
simp_rw [monotoneOn_or_antitoneOn_iff_uIcc, ← segment_eq_uIcc]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝¹ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → β
inst✝ : LinearOrder β
hf : QuasilinearOn 𝕜 s f
⊢ ∀ (a : 𝕜), a ∈ s → ∀ (b : 𝕜), b ∈ s → ∀ (c : 𝕜), c ∈ s → c ∈ segment 𝕜 a b → f c ∈ uIcc (f a) (f b)
[PROOFSTEP]
rintro a ha b hb c _ h
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝¹ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → β
inst✝ : LinearOrder β
hf : QuasilinearOn 𝕜 s f
a : 𝕜
ha : a ∈ s
b : 𝕜
hb : b ∈ s
c : 𝕜
x✝ : c ∈ s
h : c ∈ segment 𝕜 a b
⊢ f c ∈ uIcc (f a) (f b)
[PROOFSTEP]
refine' ⟨((hf.2 _).segment_subset _ _ h).2, ((hf.1 _).segment_subset _ _ h).2⟩
[GOAL]
case refine'_1
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝¹ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → β
inst✝ : LinearOrder β
hf : QuasilinearOn 𝕜 s f
a : 𝕜
ha : a ∈ s
b : 𝕜
hb : b ∈ s
c : 𝕜
x✝ : c ∈ s
h : c ∈ segment 𝕜 a b
⊢ a ∈ {x | x ∈ s ∧ f a ⊓ f b ≤ f x}
[PROOFSTEP]
simp [*]
[GOAL]
case refine'_2
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝¹ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → β
inst✝ : LinearOrder β
hf : QuasilinearOn 𝕜 s f
a : 𝕜
ha : a ∈ s
b : 𝕜
hb : b ∈ s
c : 𝕜
x✝ : c ∈ s
h : c ∈ segment 𝕜 a b
⊢ b ∈ {x | x ∈ s ∧ f a ⊓ f b ≤ f x}
[PROOFSTEP]
simp [*]
[GOAL]
case refine'_3
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝¹ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → β
inst✝ : LinearOrder β
hf : QuasilinearOn 𝕜 s f
a : 𝕜
ha : a ∈ s
b : 𝕜
hb : b ∈ s
c : 𝕜
x✝ : c ∈ s
h : c ∈ segment 𝕜 a b
⊢ a ∈ {x | x ∈ s ∧ f x ≤ f a ⊔ f b}
[PROOFSTEP]
simp [*]
[GOAL]
case refine'_4
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝¹ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → β
inst✝ : LinearOrder β
hf : QuasilinearOn 𝕜 s f
a : 𝕜
ha : a ∈ s
b : 𝕜
hb : b ∈ s
c : 𝕜
x✝ : c ∈ s
h : c ∈ segment 𝕜 a b
⊢ b ∈ {x | x ∈ s ∧ f x ≤ f a ⊔ f b}
[PROOFSTEP]
simp [*]