Random fake analysis stuff

Changes

1 changed files (+94/-9)

• Analysis.lean
  • @@ -1,12 +1,97 @@
    import Mathlib - example (x : ℝ) (h : 0 ≤ x) (hn : ∀ n, x ≤ 1 / n) : x = 0 := by + example (x : ℝ) (h : 0 ≤ x) (hn : ∀ n : ℕ, n > 0 → x ≤ 1 / n) : x = 0 := by + by_contra + have : 0 < 2 / x := (lt_div_iff₀ (by grind)).mpr (by grind) + have := hn (Nat.ceil (2 / x)) (Nat.ceil_pos.mpr this) + suffices x > 1 / (Nat.ceil (2 / x)) by linarith + have := Nat.le_ceil (2 / x) + have : 1 / x < Nat.ceil (2 / x) := by grind + have := inv_strictAnti₀ (by grind) this + field_simp at this + exact this + + + example (x : ℝ) (h : 0 ≤ x) (hn : ∀ n : ℕ, x ≤ 1 / n) : x = 0 := by by_contra - have := hn <| Nat.ceil (2 / x) - have : x > 1 / (Nat.ceil (2 / x)) := by - have := Nat.le_ceil (2 / x) - have : 1 / x < Nat.ceil (2 / x) := by grind - have := inv_strictAnti₀ (by grind) this - field_simp at this - exact this - linarith + have : 0 < 2 / x := (lt_div_iff₀ (by grind)).mpr (by grind) + have := hn (Nat.ceil (2 / x)) + suffices x > 1 / (Nat.ceil (2 / x)) by grind + have := Nat.le_ceil (2 / x) + have : 1 / x < Nat.ceil (2 / x) := by grind + have := inv_strictAnti₀ (by grind) this + field_simp at this + exact this + + + example (x : ℝ) (h : 0 ≤ x) (hn : ∀ n, x ≤ 1 / n) : x = 0 := by + linarith [hn 0] + + + + lemma blah3 (x : ℝ) (h : 0 ≤ x) (hn : ∀ n, x ≤ 1 / n) : x = 0 := by + have := hn 0 + simp at this + exact le_antisymm this h + + #print blah3 + + + lemma blah4 (x : ℝ) (h : 0 ≤ x) (hn : ∀ n, x ≤ 1 / n) : x = 0 := + le_antisymm (Eq.mp (congrArg (LE.le x) (div_zero 1)) (hn 0)) h + + + -- example (x : ℝ) (h : 0 ≤ x) (hn : ∀ n : ℕ, x ≤ 1 / n) : x = 0 := by + + -- have h₁ : x ≤ 1 := by + -- have h₂ := hn 1 + -- norm_num at h₂ ⊢ + -- <;> linarith + -- have h₂ : x = 0 := by + -- by_contra h₃ + -- -- We will show that if x ≠ 0, then there exists a natural number n such that x > 1 / n, contradicting hn. + -- have h₄ : 0 < x := lt_of_le_of_ne h (Ne.symm h₃) + -- -- Since x > 0, we can find a natural number n such that x > 1 / n. + -- have h₅ : ∃ n : ℕ, x > 1 / n := by + -- -- Choose n = ⌈2 / x⌉₊. + -- use ⌈(2 : ℝ) / x⌉₊ + -- have h₆ : (x : ℝ) > 0 := by exact_mod_cast h₄ + -- have h₇ : (⌈(2 : ℝ) / x⌉₊ : ℝ) ≥ (2 : ℝ) / x := Nat.le_ceil _ + -- have h₈ : (1 : ℝ) / ⌈(2 : ℝ) / x⌉₊ ≤ 1 / ((2 : ℝ) / x) := by + -- apply one_div_le_one_div_of_le + -- · positivity + -- · linarith + -- have h₉ : (1 : ℝ) / ((2 : ℝ) / x) = x / 2 := by + -- field_simp + -- <;> ring + -- <;> field_simp + -- <;> linarith + -- have h₁₀ : (1 : ℝ) / ⌈(2 : ℝ) / x⌉₊ ≤ x / 2 := by linarith + -- have h₁₁ : x > 1 / ⌈(2 : ℝ) / x⌉₊ := by + -- have h₁₂ : (x : ℝ) > 0 := by exact_mod_cast h₄ + -- have h₁₃ : (⌈(2 : ℝ) / x⌉₊ : ℝ) ≥ (2 : ℝ) / x := Nat.le_ceil _ + -- have h₁₄ : (1 : ℝ) / ⌈(2 : ℝ) / x⌉₊ ≤ x / 2 := by linarith + -- have h₁₅ : x > 1 / ⌈(2 : ℝ) / x⌉₊ := by + -- by_contra h₁₆ + -- have h₁₇ : (x : ℝ) ≤ 1 / ⌈(2 : ℝ) / x⌉₊ := by linarith + -- have h₁₈ : (⌈(2 : ℝ) / x⌉₊ : ℝ) ≥ (2 : ℝ) / x := Nat.le_ceil _ + -- have h₁₉ : (x : ℝ) * ⌈(2 : ℝ) / x⌉₊ ≤ 1 := by + -- calc + -- (x : ℝ) * ⌈(2 : ℝ) / x⌉₊ ≤ (1 / ⌈(2 : ℝ) / x⌉₊) * ⌈(2 : ℝ) / x⌉₊ := by gcongr <;> linarith + -- _ = 1 := by field_simp [Nat.cast_ne_zero.mpr (by positivity : ⌈(2 : ℝ) / x⌉₊ ≠ 0)] <;> ring + -- have h₂₀ : (x : ℝ) * ⌈(2 : ℝ) / x⌉₊ ≥ (x : ℝ) * ((2 : ℝ) / x) := by + -- gcongr <;> linarith + -- have h₂₁ : (x : ℝ) * ((2 : ℝ) / x) = 2 := by + -- field_simp [h₆.ne'] + -- <;> ring + -- <;> field_simp [h₆.ne'] + -- <;> linarith + -- linarith + -- exact_mod_cast h₁₅ + -- exact h₁₁ + -- -- Obtain the natural number n such that x > 1 / n. + -- obtain ⟨n, hn'⟩ := h₅ + -- have h₆ := hn n + -- -- This leads to a contradiction because x ≤ 1 / n by assumption, but we have x > 1 / n. + -- linarith + -- exact h₂