a problem

Stream: new members

[tsuki hao]

import Mathlib.Tactic
import Mathlib.Data.Real.Basic

example (h : a ≤ b) : log (1 + exp a) ≤ log (1 + exp b) := by
  have h₀ : 0 < 1 +exp a :=by sorry
  have h₁ : 0 < 1 +exp b :=by sorry
  apply (log_le_log h₀ h₁).mpr
  sorry

Does anyone know how to complete this code？

[Kevin Buzzard]

I would guess that there will be a lemma called something like docs#Real.exp_pos which might help?

[Jeremy Tan]

import Mathlib.Analysis.SpecialFunctions.Log.Basic

namespace Real

variable {x y : ℝ}

example (h : x < y) : log (1 + exp x) < log (1 + exp y) := by
  have ha : 0 < 1 + exp x := by positivity
  have hb : 0 < 1 + exp y := by positivity
  apply (strictMonoOn_log.lt_iff_lt ha hb).mpr
  simpa

end Real

[Jeremy Tan]

One-liner:

import Mathlib.Analysis.SpecialFunctions.Log.Basic

namespace Real

variable {x y : ℝ}

example (h : x < y) : log (1 + exp x) < log (1 + exp y) :=
  log_lt_log (by positivity) (by simpa)

end Real

[Jeremy Tan]

In mathlib, to cut down on variable use and generalise, your theorem would be written like this:

import Mathlib.Analysis.SpecialFunctions.Log.Basic

namespace Real

theorem strictMono_softplus : StrictMono fun x => log (1 + exp x) := by
  unfold StrictMono
  intros
  exact log_lt_log (by positivity) (by simpa)

end Real

[Heather Macbeth]

Come on @Kevin Buzzard @Jeremy Tan, this is not the modern way to do this!

import Mathlib.Analysis.SpecialFunctions.Log.Basic

open Real

-- missing `gcongr` lemmas
alias log_le_log ↔ _ log_le_log_of_le
alias exp_le_exp ↔ _ exp_le_exp_of_le
attribute [gcongr] log_le_log_of_le exp_le_exp_of_le

example (h : a ≤ b) : log (1 + exp a) ≤ log (1 + exp b) := by gcongr

[Jeremy Tan]

The newcomer probably doesn't know what gcongr does

[Heather Macbeth]

example (h : a ≤ b) : log (1 + exp a) ≤ log (1 + exp b) := by rel [h]

if you prefer. If you can understand rw then you can understand gcongr.

[tsuki hao]

Thank you all for your help, I can now solve this problem!

[tsuki hao]

import Mathlib.Tactic
import Mathlib.Data.Real.Basic
import Mathlib.Data.Nat.Prime

open Real

namespace S04

variable (x y : ℝ)
example  {x y :ℝ} (h₀ : x ≤ y) (h₁ : ¬ y ≤ x) : x ≤ y ∧ x ≠ y := by
  constructor
  · assumption
  intro h
  apply h₁
  rw[h]

Does anyone know why I wrote this wrong?

[Scott Morrison]

@tsuki hao, that seems fine to me. Can you explain why you think something is wrong?

[tsuki hao]

Scott Morrison said:

tsuki hao, that seems fine to me. Can you explain why you think something is wrong?

I'm sorry this is my problem, there is an error in another part.

[tsuki hao]

variable (x : ℕ)
theorem convergesTo_const (a : ℝ) : ConvergesTo (fun x : ℕ ↦ a) a := by
  intro ε εpos
  use 0
  intro n nge
  rw [sub_self, abs_zero]
  apply εpos

Can I ask why this gives 'tactic 'introN' failed' error

[Scott Morrison]

#mwe, please! :-)

[tsuki hao]

Scott Morrison said:

#mwe, please! :-)

import Mathlib.Tactic
import Mathlib.Data.Real.Basic
open Real

def ConvergesTo (s : ℕ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ N ,∀ n ≥ N, |s n - a|< ε

variable (x : ℕ)
theorem convergesTo_const (a : ℝ) : ConvergesTo (fun x : ℕ ↦ a) a := by
  intro ε εpos
  use 0
  intro n nge
  rw [sub_self, abs_zero]
  apply εpos

Sorry, and can I ask what it mean by use 0 here

[Kevin Buzzard]

If your goal is an exists (there exists an X such that blah(X)) then use 0 is the claim that X=0 works so your goal changes to blah(0). Note that it can turn true goals into false ones if used incorrectly.

[tsuki hao]

Does anyone know how to formulate the problem: All elements on the intersection of the finite group and the unit group of the complex filed have modulo 1?

[Johan Commelin]

Do you mean

example (G : Subgroup (Units ℂ)) (hG : Finite G) (x : Units ℂ) (hx : x ∈ G) :
  ‖(x : ℂ)‖ = 1 := sorry

[tsuki hao]

Johan Commelin said:

Do you mean

example (G : Subgroup (Units ℂ)) (hG : Finite G) (x : Units ℂ) (hx : x ∈ G) :
  ‖(x : ℂ)‖ = 1 := sorry

Thank you very much! That's exactly what I meant!

[tsuki hao]

May I ask if there is a theorem that any element in a finite group，its order is bounded in lean?

[Kevin Buzzard]

Sure there are many theorems in mathlib about orders of elements. Why don't you figure out how to search the library yourself? Click on the magnifying glass on GitHub and type "order of element" or "order of the element" or "order of an element" and see what you find. Don't ever seem to get any results? Click on the three dots near the search window and then click on the blue cog to make it not blue.

[tsuki hao]

Kevin Buzzard said:

Sure there are many theorems in mathlib about orders of elements. Why don't you figure out how to search the library yourself? Click on the magnifying glass on GitHub and type "order of element" or "order of the element" or "order of an element" and see what you find. Don't ever seem to get any results? Click on the three dots near the search window and then click on the blue cog to make it not blue.

Thank you!

[Notification Bot]

tsuki hao has marked this topic as resolved.

[Notification Bot]

Billlie Franch has marked this topic as unresolved.

[Yaël Dillies]

If you want the answer, I proved this just yesterday for my project.

[tsuki hao]

Yaël Dillies said:

If you want the answer, I proved this just yesterday for my project.

That would be great ！ can I have a look at your proof？

[Yury G. Kudryashov]

Here is an informal outline of the proof:

• use docs#exists_pow_eq_one and docs#isOfFinOrder_iff_coe to show that x has finite order.
• since x ^ n = 1, we have ‖x‖ ^ n = 1, thus ‖x‖ = 1

[Yury G. Kudryashov]

The second step could be formulated as

theorem IsOfFinOrder.norm_eq_one {K : Type _} [NormedDivisionRing K] {a : K} (ha : IsOfFinOrder a) :
    ‖a‖ = 1 := _

[Notification Bot]

tsuki hao has marked this topic as resolved.

[tsuki hao]

Yury G. Kudryashov said:

Here is an informal outline of the proof:

• use docs#exists_pow_eq_one and docs#isOfFinOrder_iff_coe to show that x has finite order.
• since x ^ n = 1, we have ‖x‖ ^ n = 1, thus ‖x‖ = 1

Thank you very much!

[tsuki hao]

import Mathlib.Tactic
import Mathlib.Algebra.Group.Basic
import Mathlib.GroupTheory.Subgroup.Basic
import Mathlib.Data.Real.Basic

example (a b : Nat)(h : a ∣ b - (b - 1)) : a ∣ 1 := by
  sorry

Can someone prove this proposition?

[Riccardo Brasca]

What have you tried so far? The point is to prove that b - (b - 1) = 1. This is surely in the library in some form or another, it's even possible that exact? is able to do it.

[tsuki hao]

Riccardo Brasca said:

What have you tried so far? The point is to prove that b - (b - 1) = 1. This is surely in the library in some form or another, it's even possible that exact? is able to do it.

I tried apply? and exact? but didn’t find the tactic I want, I want to use rw but I don’t know how to use it

[Eric Wieser]

Have you tried to prove b - (b - 1) = 1 in isolation?

[Eric Wieser]

This is surely in the library in some form or another

Not in the form you stated, as it's false when b = 0!

[Riccardo Brasca]

Ops, you're right

[Kevin Buzzard]

so in fact the example as stated can't be proved, as a=2 and b=0 is a counterexample.

[tsuki hao]

import Mathlib.Tactic
import Mathlib.Algebra.Group.Basic
import Mathlib.GroupTheory.Subgroup.Basic
import Mathlib.Data.Real.Basic

example (a b : Nat)(h : a ∣ b - (b - 1)) : a ∣ 1 := by
  have h1 : b - (b - 1) = 1 := by
    sorry
  rw[h1] at h
  exact h

Is it not possible to prove it in this form? I don’t understand it.

[Ruben Van de Velde]

If b = 0, then b - (b - 1) = 0 - (0 - 1) = 0 - 0 = 0

[tsuki hao]

Ruben Van de Velde said:

If b = 0, then b - (b - 1) = 0 - (0 - 1) = 0 - 0 = 0

Thank you!

[Notification Bot]

tsuki hao has marked this topic as resolved.

[Notification Bot]

Scott Morrison has marked this topic as unresolved.

[Scott Morrison]

Note that on the original question, slim_check immediately identifies the problem:

import Mathlib.Tactic
import Mathlib.Algebra.Group.Basic
import Mathlib.GroupTheory.Subgroup.Basic
import Mathlib.Data.Real.Basic

example (a b : Nat)(h : a ∣ b - (b - 1)) : a ∣ 1 := by
  slim_check

[Scott Morrison]

We really need to be running exact? and slim_check in the infoview automatically whenever your cursor rests at a sorry. :-)

[Kevin Buzzard]

And simp and aesop

[Eric Wieser]

How about a zulip bot that does that?

[tsuki hao]

Scott Morrison said:

Note that on the original question, slim_check immediately identifies the problem:

import Mathlib.Tactic
import Mathlib.Algebra.Group.Basic
import Mathlib.GroupTheory.Subgroup.Basic
import Mathlib.Data.Real.Basic

example (a b : Nat)(h : a ∣ b - (b - 1)) : a ∣ 1 := by
  slim_check

Thank you!

[Billlie Franch]

I would like to ask the three kinds of brackets in lean4, what are the uses of (), [], and {} respectively

[Mario Carneiro]

• () are for explicit arguments, you pass these normally to a function like f x
• {} are for implicit arguments, you don't pass these yourself, lean figures them out as though you wrote f _
• [] are for instance implicit arguments, you also don't pass these manually but they are found by type class inference instead of unification
• {{}} are semi-implicit arguments, these act like implicits unless you use the term unapplied, meaning that f acts like f and f x acts like f _ x if the first argument is semi-implicit and the second argument is explicit

[Mario Carneiro]

if you put @ before a function name then all parameters are treated as explicit

[Mario Carneiro]

and you can always pass a parameter by name as in f (a := x) even if it is implicit

[Billlie Franch]

I would like to ask if there is any trick to use [] and <> when using rintro
In addition, can I ask if there is any useful tactic in proving the set contains relationship
Thanks