FKS2.find_ereal_bin

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, _⟩.