Small sorrys help

Stream: new members

[rtertr (Sonia)]

Hello everyone,

I have the following small sorry's that I struggle to resolve, and that I have not been able to find theorems in the Mathlib.
The first one is about disjoint sets, saying that [-a,a] and (a,infinity) are disjoint.
The next one is about type conversion. Delta is real, but cast as complex, and I need to show that 1 and 2 are both natural and complex numbers.
The third one is about the limit of a real number going to zero, but the number is cast as a complex number.
And the last one is about arctan going to pi/2.
Any help would be greatly appreciated! Here is the minimal code:
Kind regards!

import tactic
import analysis.special_functions.gaussian

section
open set
open set filter
open real

noncomputable theory

namespace real

lemma Icc_disjoint_Iio {μ:ℝ} (h: 0≤ μ): disjoint (Icc (-μ) μ) (Ioi μ):=
begin
  sorry,
end

lemma pow_complex_to_natural {δ:ℝ }: (δ:ℂ) ^ ((1:ℂ)/(2:ℂ)) = (δ:ℂ) ^ ((1:ℕ)/(2:ℕ)):=
begin
  sorry,
end

lemma tendsto_coe:tendsto (λ (k : ℝ), (k:ℂ )) (nhds_within 0 (Ioi 0)) (nhds 0):=
begin
  simp only,
  sorry,
end

lemma tendsto_arctan_at_top: tendsto (λ (k : ℝ), arctan k) at_top (nhds (real.pi / 2)):=
begin
  sorry,
end

[Kevin Buzzard]

I doubt the second one is true, because (1 : nat) / (2 : nat) = 0 : nat

[Ruben Van de Velde]

For the first:

lemma Icc_disjoint_Iio {μ:ℝ} (h: 0≤ μ): disjoint (Icc (-μ) μ) (Ioi μ):=
begin
  intros s h1 h2,
  simp [set.subset_empty_iff, set.eq_empty_iff_forall_not_mem],
  intros x hx,
  specialize h1 hx,
  specialize h2 hx,
  simp at h1 h2,
  linarith,
end

[rtertr (Sonia)]

Kevin Buzzard said:

I doubt the second one is true, because (1 : nat) / (2 : nat) = 0 : nat

Ah okay, then there must be something wrong else where in my proof! :D

[rtertr (Sonia)]

Ruben Van de Velde said:

For the first:

Thank you! :D :tada: :tada: :tada:

[Eric Wieser]

intros is generally the wrong way to prove disjoint

[Eric Wieser]

(it used to be, but the definition changed to be more general and is now inconvenient)

[Yaël Dillies]

Eric, do you think we should have made disjoint and codisjoint structures to avoid people trying to intro into them?

[Eric Wieser]

Maybe, though then they'd just use split

[Eric Wieser]

In this case docs#set.Iic_disjoint_Ioi (and monotonicity) provides a much shorter proof

[Yaël Dillies]

I quite like the idea because it also matches the status of docs#is_compl

[Kevin Buzzard]

A nontrivial percentage of my Lean 3 students would use fconstructor (which comes up so often that I suspect that one of those super-generic tactics like hint is suggesting it)

[Yaël Dillies]

Oh that's really surprising. I literally never used fconstructor.

[Kevin Buzzard]

yeah me neither, but probably you are not trying to write a Lean project as part of your degree when you'd never used the language three weeks before...

[Eric Wieser]

Eric Wieser said:

In this case docs#set.Iic_disjoint_Ioi (and monotonicity) provides a much shorter proof

lemma Icc_disjoint_Iio {μ:ℝ} : disjoint (Icc (-μ) μ) (Ioi μ):=
(set.Iic_disjoint_Ioi le_rfl).mono_left set.Icc_subset_Iic_self

didn't even need your h

[Eric Wieser]

Another one:

lemma tendsto_coe : tendsto (λ k : ℝ, (k : ℂ)) (nhds_within 0 (Ioi 0)) (nhds 0) :=
(complex.continuous_of_real.tendsto' 0 _ complex.of_real_zero).mono_left nhds_within_le_nhds

[rtertr (Sonia)]

Eric Wieser said:

Another one:

Wow, great! Thank you! I might write about it in my thesis. Can I write your name to credit you, or do you have any privacy concerns? It will just be read by my two advisors, btw :) I will also write a credit in my PR, ofc as well.

[Eric Wieser]

My name is already plastered all over mathlib header comments, so feel free to

[rtertr (Sonia)]

I guess, this is a general question. How do you give credit to people who helped you on Zulip without potentially causing privacy issues? :) Do you normally write all the usernames of the people who helped or how so? :)

[Eric Wieser]

Zulip is public anyway, so I think any personal info written in web-public channels here is probably fair game to include elsewhere (but it does no harm to check)

[Eric Wieser]

I tried the last one too, but I'm not familiar enough with filters to know if the last sorry is true:

lemma tendsto_arctan_at_top: tendsto (λ (k : ℝ), arctan k) at_top (nhds (real.pi / 2)):=
begin
  simp_rw arctan,
  refine tendsto.comp _ (order_iso.tendsto_at_top _),
  sorry
end

[rtertr (Sonia)]

Thank you! :D

[Eric Wieser]

With the sorry slightly abstracted:

lemma at_top_eq_nhds_within (a b : ℝ) :  (at_top : filter (set.Ioo a b)) = (𝓝[≤] b).comap coe :=
sorry -- this might not be true!

lemma tendsto_arctan_at_top: tendsto (λ (k : ℝ), arctan k) at_top (nhds (real.pi / 2)):=
begin
  simp_rw arctan,
  apply tendsto.comp _ (order_iso.tendsto_at_top _),
  rw at_top_eq_nhds_within,
  exact tendsto_comap.mono_right nhds_within_le_nhds,
end

[Eric Wieser]

I made a new thread for that sorry

[Julian Berman]

Kevin Buzzard said:

A nontrivial percentage of my Lean 3 students would use fconstructor (which comes up so often that I suspect that one of those super-generic tactics like hint is suggesting it)

(This is precisely it, or was for me, fconstructor shows up constantly in hint and I had to learn it was useless after seeing it so often and never having it get me anywhere I couldn't have already gotten to)

[Kevin Buzzard]

I knew it would be something like that!

[rtertr (Sonia)]

Good evening everyone,
I have another small sorry question!
Just trying to prove the following:

import tactic
import analysis.special_functions.gaussian

section
open real

noncomputable theory

namespace real

theorem complex_coe_ne_zero {δ:ℝ } (hδ: 0<δ): (δ:ℂ ) ≠ 0:=
begin
  norm_cast,
  sorry,
end

[David Renshaw]

  exact ne_of_gt hδ

[David Renshaw]

(That's what the library_search tactic told me to do.)

[rtertr (Sonia)]

Oh, great! Mine just timed-out, so I guess I should extend the thinking time :D :tada:

[David Renshaw]

Hm... yeah I see that my .emacs does have a line (setq lean-timeout-limit 1000000), so maybe that's why mine didn't time out.

[rtertr (Sonia)]

well, thank you for the time then haha!

[Kevin Buzzard]

Maybe one of exact hδ.ne or exact hδ.ne'works. Or even exact_mod_cast hδ.ne' is a one-liner?

Note that in Lean 4 library_search is much faster (and is called exact?). Time to upgrade? ;-)