FKS2.ereal_exp_ge_max

This follows by combining the three substeps. -/) (latexEnv := "theorem") (discussion := 718)] theorem theorem_6_alt {x₀ x₁ : ℝ} (h : x₁ ≥ max x₀ 14) {N : ℕ} (b : Fin (N + 1) → ℝ) (hmono : Monotone b) (h_b_start : b 0 = log x₀) (h_b_end : b (Fin.last N) = log x₁) (εθ_num : ℝ → ℝ) (h_εθ_num : ∀ i : Fin (N+1), Eθ.numericalBound (exp (b i)) εθ_num) (x : ℝ) (hx₁ : x₁ ≤ x) (hx₀ : x₀ ≥ 2) : Eπ x ≤ εθ_num x₁ * (1 + μ_num_2 b εθ_num x₀ x₁) := by have h6 := theorem_6 (⊤ : EReal) h b hmono h_b_start h_b_end εθ_num h_εθ_num x hx₁ le_top hx₀ suffices hsuff : μ_num b εθ_num x₀ x₁ (⊤ : EReal) = μ_num_2 b εθ_num x₀ x₁ by have heq : επ_num b εθ_num x₀ x₁ ⊤ = εθ_num x₁ * (1 + μ_num_2 b εθ_num x₀ x₁) := by dsimp [επ_num]; rw [hsuff] linarith dsimp [μ_num]; rfl

/-The following lemmas are used for corollary_8. -/

/- PROBLEM Helper: In a monotone EReal sequence with first element finite and last element ⊤, for any real value v ≥ b'(0), we can find a bin index i < last such that b'(i) ≤ v and v < b'(i+1).

PROVIDED SOLUTION By strong induction on M. When M = 0, Fin 0 is empty so we can't form a Fin M, but b'(0) = b'(Fin.last 0) = ⊤ and hv says v ≥ ⊤ which is impossible for real v - contradiction.

For M+1: If v < b'⟨1, ⟩, then i = ⟨0, ⟩ works since b'⟨0,⟩ ≤ v (from hv) and v < b'⟨1,⟩. Otherwise v ≥ b'⟨1,_⟩, and we can apply the result to the shifted sequence b'' = b' ∘ Fin.succ (which has M+1 elements, is monotone, ends at ⊤, and b''(0) = b'(1) ≤ v). This gives i' : Fin M with the bounds, and we take i = ⟨i'.val + 1, _⟩. -/ lemma find_ereal_bin {M : ℕ} (b' : Fin (M + 1) → EReal) (h_end : b' (Fin.last M) = ⊤) (v : ℝ) (hv : (v : EReal) ≥ b' 0) : ∃ i : Fin M, b' ⟨i.val, by omega⟩ ≤ (v : EReal) ∧ (v : EReal) < b' ⟨i.val + 1, by omega⟩ := by by_contra! h_contra; -- By induction on $i$, we can show that $b' i \leq v$ for all $i$. have h_ind : ∀ i : Fin (M + 1), b' i ≤ v := by intro i; induction i using Fin.inductionOn <;> aesop; exact absurd ( h_ind ( Fin.last M ) ) ( by simp +decide [ h_end ] )

/- PROBLEM Helper: Given a monotone EReal sequence b' and an index i such that b'(i) ≤ v (finite), the sub-partition (toReal of b' restricted to first i+1 elements) is monotone, provided all values b'(j) for j ≤ i are between b'(0) and v.

PROVIDED SOLUTION For j₁ ≤ j₂ in Fin (i.val + 1), we have ⟨j₁.val, _⟩ ≤ ⟨j₂.val, _⟩ as Fin (M+1), so b'(j₁) ≤ b'(j₂) by monotonicity of b'. Both values are finite: they are ≥ b'(0) ≠ ⊥ (by monotonicity, since j₁ ≥ 0), and ≤ b'(i) ≤ v (finite) so ≠ ⊤. Since both are finite EReal values with b'(j₁) ≤ b'(j₂), we get toReal(b'(j₁)) ≤ toReal(b'(j₂)) by EReal.toReal_le_toReal (for finite values, toReal preserves order). -/ lemma ereal_toReal_sub_mono {M : ℕ} (b' : Fin (M + 1) → EReal) (hmono : Monotone b') (i : Fin M) (v : ℝ) (hv : b' ⟨i.val, by omega⟩ ≤ (v : EReal)) (h_bot : b' 0 ≠ ⊥) : Monotone (fun j : Fin (i.val + 1) ↦ (b' ⟨j.val, by omega⟩).toReal) := by intro j k hjk generalize_proofs at *; apply EReal.toReal_le_toReal all_goals generalize_proofs at *; · exact hmono hjk; · exact ne_of_gt ( lt_of_lt_of_le ( lt_of_le_of_ne ( bot_le ) ( Ne.symm h_bot ) ) ( hmono ( Nat.zero_le _ ) ) ); · have := hmono ( show ⟨ k, by linarith ⟩ ≤ ⟨ i, by linarith ⟩ from Nat.le_of_lt_succ <| by linarith [ Fin.is_lt k, Fin.is_lt i ] ) ; aesop;

/- PROBLEM Helper: EReal.toReal of a real cast is the original value

PROVIDED SOLUTION Since h_b_start : b' 0 = ↑(log x₁), we have (b' 0).toReal = (↑(log x₁)).toReal = log x₁ by EReal.toReal_coe. -/ lemma ereal_toReal_coe_log {x₁ : ℝ} {M : ℕ} (b' : Fin (M + 1) → EReal) (h_b_start : b' 0 = ↑(log x₁)) : (b' 0).toReal = log x₁ := by aesop

/- PROBLEM Helper: for a real v, if b'(i) ≤ v and b'(0) is a finite real cast, then exp(b'(i).toReal) ≤ exp v

PROVIDED SOLUTION Since b'(0) ≠ ⊥ and b' is monotone, b'(i) ≥ b'(0) > ⊥, so b'(i) ≠ ⊥. Also b'(i) ≤ ↑v, so b'(i) ≠ ⊤ (since ↑v < ⊤). Therefore b'(i) is a finite EReal value with b'(i) ≤ ↑v, which means b'(i).toReal ≤ v by EReal.toReal_le_toReal (or similar). Then exp is monotone, so exp(b'(i).toReal) ≤ exp(v). -/ lemma ereal_exp_toReal_le {M : ℕ} (b' : Fin (M + 1) → EReal) (hmono : Monotone b') (i : Fin M) (v : ℝ) (hv : b' ⟨i.val, by omega⟩ ≤ (v : EReal)) (h_bot : b' 0 ≠ ⊥) : exp (b' ⟨i.val, by omega⟩).toReal ≤ exp v := by by_cases hi : b' ⟨i, by omega⟩ = ⊥ <;> by_cases hi' : b' ⟨i, by omega⟩ = ⊤; · aesop; · have := hmono ( show 0 ≤ ⟨ i, by linarith [ Fin.is_lt i ] ⟩ from Nat.zero_le _ ) ; aesop; · aesop; · cases h : b' ⟨ i, by linarith [ Fin.is_lt i ] ⟩ · aesop · aesop · contradiction

/- PROBLEM Helper: if b'(i) is finite (≠ ⊤) and b' is monotone with b'(0) = log x₁ where x₁ ≥ 14, then exp(b'(i).toReal) ≥ max x₁ 14

PROVIDED SOLUTION Since b' is monotone and i.val ≥ 0, b'(i) ≥ b'(0) = ↑(log x₁). Since b'(i) ≠ ⊤ and b'(i) ≥ ↑(log x₁) (which is finite, so b'(i) ≠ ⊥ too), b'(i) is a finite EReal. Therefore b'(i).toReal ≥ (b'(0)).toReal = log x₁ (using EReal.toReal_le_toReal with the ≠ ⊤ and ≠ ⊥ conditions). Since exp is monotone, exp(b'(i).toReal) ≥ exp(log x₁) = x₁ (using Real.exp_log, noting x₁ > 0 since x₁ ≥ 14). Also x₁ ≥ 14, so max x₁ 14 = x₁. Therefore exp(b'(i).toReal) ≥ max x₁ 14.