Formalize the limit and check the answer

Stream: new members

[Nick_adfor]

import Mathlib

open Real

noncomputable def f (x : ℝ) : ℝ :=

  limUnder atTop (λ n : ℕ, (cos x ^ n + sin x ^ n) ^ (1 / n))

theorem part_1 : ∀ x ∈ Set.Icc 0 (π / 2), f x = max (cos x) (sin x) := by sorry

I want to formalize the limit of (cos x ^ n + sin x ^ n) ^ (1 / n) and check the answer f(x). (I don't want to calculate the answer in Lean because I think it may be hard for lean to calculate this.) But Lean has an error:

unexpected token ','; expected '↦', '=>'

"," is "λ n : ℕ, " here. Experience tells me that the error in Lean Infoview can't tell me where the grammar is wrong. So I seek help here.

Thank you!

[Zhang Qinchuan]

Your code is not #mwe. Seems you are writing random code and hoping it can compile. Just read TPIL to learn the basic grammar.

And read MIL to learn the concept of docs#Filter.Tendsto .

[Nick_adfor]

Zhang Qinchuan said:

Your code is not #mwe. Seems you are writing random code and hoping it can compile. Just read TPIL to learn the basic grammar.

And read MIL to learn the concept of docs#Filter.Tendsto .

Oh...Seems that the definition of limit in Lean is a little difficult

[Zhang Qinchuan]

Nick_adfor said:

Oh...Seems that he definition of limit is a little difficult

Most people is familiar with $\varepsilon-\delta$, but Mathlib says docs#Filter is more powerful once you get used to.

You can try to the following code:

import Mathlib

open Real Filter Topology

lemma exists_tendsto (x : ℝ) : ∃ c : ℝ,
    Tendsto (fun n : ℕ => (cos x ^ n + sin x ^ n) ^ (1 / n : ℝ)) atTop (𝓝 c) := by
  sorry

noncomputable def f (x : ℝ) : ℝ := Classical.choose (exists_tendsto x)

theorem part_1 : ∀ x ∈ Set.Icc 0 (π / 2), f x = max (cos x) (sin x) := by sorry

[Aaron Liu]

Here's what I came up with

import Mathlib

open Real Filter Topology

-- This statement simultaneously asserts that the limit exists and is equal to `max (cos x) (sin x)`.
example
    -- forall real numbers `0 ≤ x ≤ π / 2`
    (x : ℝ) (hx : x ∈ Set.Icc 0 (π / 2)) :

    -- in the limit
    Tendsto

    -- the sequence `fₙ = ⁿ√(cos x ^ n + sin x ^ n)`
    (fun (n : Nat) ↦ (cos x ^ n + sin x ^ n) ^ (n⁻¹ : ℝ))

    -- as `n → ∞`
    atTop

    -- approaches `max (cos x) (sin x)`
    (𝓝 (max (cos x) (sin x))) := by
  sorry

-- The reason we use `Tendsto` is that small variations on the statement do not require a new definition.
example
    -- forall real numbers `0 ≤ x ≤ π / 2`
    (x : ℝ) (hx : x ∈ Set.Icc 0 (π / 2)) :

    -- in the limit
    Tendsto

    -- the sequence `fₙ = ⁿ√(cos x ^ n + sin x ^ n)`
    (fun (n : Nat) ↦ (cos x ^ n + sin x ^ n) ^ (n⁻¹ : ℝ))

    -- as `n → ∞`
    atTop

    -- approaches `max (cos x) (sin x)` from the left
    (𝓝[≤] (max (cos x) (sin x))) := by
  sorry

[Nick_adfor]

Zhang Qinchuan said:

Nick_adfor said:

Oh...Seems that the definition of limit in lean is a little difficult

Most people is familiar with $\varepsilon-\delta$, but Mathlib says docs#Filter is more powerful once you get used to.

You can try to the following code:

import Mathlib

open Real Filter Topology

lemma exists_tendsto (x : ℝ) : ∃ c : ℝ,
    Tendsto (fun n : ℕ => (cos x ^ n + sin x ^ n) ^ (1 / n : ℝ)) atTop (𝓝 c) := by
  sorry

noncomputable def f (x : ℝ) : ℝ := Classical.choose (exists_tendsto x)

theorem part_1 : ∀ x ∈ Set.Icc 0 (π / 2), f x = max (cos x) (sin x) := by sorry

Thank you for your reply! I have briefly skimmed through the code in the Filter, and its definition does seem more complex than the traditional epsilon-delta approach I learned in my analysis course. However, its scope of application also appears to be more general even in any other topology.

[Nick_adfor]

Aaron Liu said:

Here's what I came up with

import Mathlib

open Real Filter

-- This statement simultaneously asserts that the limit exists and is equal to `max (cos x) (sin x)`.
example
    -- forall real numbers `0 ≤ x ≤ π / 2`
    (x : ℝ) (hx : x ∈ Set.Icc 0 (π / 2)) :

    -- in the limit
    Tendsto

    -- the sequence `fₙ = ⁿ√(cos x ^ n + sin x ^ n)`
    (fun (n : Nat) ↦ (cos x ^ n + sin x ^ n) ^ (n⁻¹ : ℝ))

    -- as `n → ∞`
    atTop

    -- approaches `max (cos x) (sin x)`
    (nhds (max (cos x) (sin x))) := by
  sorry

Thank you, too. I'll take some time to understand "nhds"