Documentation

Lean 4 Proof

theorem finite_crossing_ivt :
    ∀ (f : ℝ → ℝ), Continuous f →
      f 0 < 1 → (∃ M : ℝ, 0 < M ∧ 1 < f M) →
      ∃ Q_star : ℝ, 0 < Q_star ∧ f Q_star = 1 := by
  intro f hf hf0 ⟨M, hM_pos, hfM⟩
  -- Apply IVT on [0, M]: f(0) < 1 < f(M)
  have hle : (0 : ℝ) ≤ M := le_of_lt hM_pos
  have hfcont : ContinuousOn f (Set.Icc 0 M) := hf.continuousOn
  have h1_mem : (1 : ℝ) ∈ Set.Icc (f 0) (f M) :=
    ⟨le_of_lt hf0, le_of_lt hfM⟩
  obtain ⟨Q_star, ⟨hQ_ge, hQ_le⟩, hfQ⟩ := intermediate_value_Icc hle hfcont h1_mem
  -- We need Q_star > 0. Since f(0) < 1 = f(Q_star), Q_star ≠ 0
  have hQ_ne : Q_star ≠ 0 := by
    intro heq; rw [heq] at hfQ; linarith
  exact ⟨Q_star, lt_of_le_of_ne hQ_ge (Ne.symm hQ_ne), hfQ⟩

Dependency Graph

Location

thesis/CESProofs/Hierarchy/EndogenousCrossing.lean:163

Module Section

Proposition: Endogenous Crossing

In the same file