FKS2.ereal_toReal_sub_mono

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).