Home for a lemma

Stream: mathlib4

[Michael Stoll]

What would be a good file for the following to go in?

lemma Complex.indicator_ofReal {f : ℕ → ℝ} {s : Set ℕ} :
    (fun n ↦ ((Set.indicator s f n : ℝ) : ℂ)) = Set.indicator s (fun n ↦ (f n : ℂ))

#find_home suggests Mathlib.Data.Complex.Abs, Mathlib.Data.Complex.Cardinality, Mathlib.Data.Complex.BigOperators, none of which looks very convincing.

[Michael Stoll]

And another one:

lemma Complex.one_add_I_mul_ne_one {y : ℝ} (hy : y ≠ 0) : 1 + I * y ≠ 1

It could go into Data.Complex.Basic, but it does not feel like a "basic" lemma. I found that I need it a couple of times in an application (which should go into Mathliib eventually); so does it make sense to have it as a Mathlin lemma, or is it better a private lemma in the file where it is used?

[Jireh Loreaux]

The second one is just docs#add_right_ne_self

[Kevin Buzzard]

(and mul_ne_zero)

[Kevin Buzzard]

It's not clear to me that the lemma is any more useful than $z+iy\not=z$

[Jireh Loreaux]

Indeed, but I think even just add_right_ne_self.mpr <| by positivity likely works (unless positivity doesn't know that I is nonzero, which is possible)

[Jireh Loreaux]

But maybe we should tell it.

[Kevin Buzzard]

But I isn't positive, right?

[Jireh Loreaux]

Positivity handles nonzeroness, no?

[Michael Stoll]

Jireh Loreaux said:

Indeed, but I think even just add_right_ne_self.mpr <| by positivity likely works (unless positivity doesn't know that I is nonzero, which is possible)

I get "failed to synthesize PartialOrder ℂ" (and with open scoped ComplexOrder, "failed to prove positivity/nonnegativity/nonzeroness"). My proof is a bit longer:

lemma one_add_I_mul_ne_one {y : ℝ} (hy : y ≠ 0) : 1 + I * y ≠ 1 := by
  simp only [ne_eq, add_right_eq_self, mul_eq_zero, I_ne_zero, ofReal_eq_zero, hy, or_self,
    not_false_eq_true]

which is why I have stated it as a separate lemma.

[Jireh Loreaux]

Ah, I forget that the partial order instance on ℂ isn't global, sorry.

[Michael Stoll]

Kevin Buzzard said:

It's not clear to me that the lemma is any more useful than $z+iy\not=z$

In my use case, there is a difference, because specializing the general lemma to $z = 1$ introduces a cast, which then prevents ring from closing whatever goal remains at that stage.

[Michael Stoll]

... but this can be remedied by a rw [ofReal_one], which I'm willing to insert if the more general lemma Kevin suggests is deemed to be a useful addition to Mathlib.

[Jireh Loreaux]

I just had a second to sit down with this. The following works, probably my suggestion of positivity was not the right one.

import Mathlib.Data.Complex.Basic

lemma Complex.one_add_I_mul_ne_one {y : ℝ} (hy : y ≠ 0) : 1 + I * y ≠ 1 :=
  add_right_ne_self.mpr <| by aesop

[Jireh Loreaux]

long live aesop

[Michael Stoll]

The asesop proof is pretty much the same as the one I had...

[Michael Stoll]

lemma add_I_mul_ne_self {x y : ℝ} (hy : y ≠ 0) : x + I * y ≠ x :=
  mt add_right_eq_self.mp fun H ↦ ofReal_ne_zero.mpr hy <| (mul_eq_zero.mp H).resolve_left I_ne_zero

is what you get by translating to a term.

[Jireh Loreaux]

okay? but the point is it's easy to write, so then why do we need the specialized lemma?

[Michael Stoll]

My use case looks like this:

lemma riemannZeta_isBigO_of_ne_one_horizontal {y : ℝ} (hy : y ≠ 0) :
    (fun x : ℝ ↦ ζ (1 + x + I * y)) =O[𝓝[>] 0] (fun _ ↦ (1 : ℂ)) := by
  refine Asymptotics.IsBigO.mono ?_ nhdsWithin_le_nhds
  convert isBigO_comp_ofReal
    (differentiableAt_riemannZeta <| add_I_mul_ne_self hy).continuousAt.isBigO using 3 with x
  rw [ofReal_one] -- not necessary with `one_add_I_mul_ne_one`
  ring

which I find nicer than providing a proof explicitly there (and at the other place where I need it).

[Jireh Loreaux]

That's not an #mwe, can you provide the open statements?

[Michael Stoll]

I think the rule is basically, if you need something at least twice (and its proof is not very short), then it makes sense as a lemma.

[Jireh Loreaux]

I think add_right_ne_self.mpr <| by aesop qualifies as "very short". But in any case, I don't want to argue about this. If you really want the lemma, feel free to include it in a PR. I'll let another maintainer disagree if they care to. If not, that's fine too.

[Michael Stoll]

It was not meant as an MWE. It is from this file and it needs isBigO_comp_ofReal from the file Auxiliary.lean in the same repo.

[Michael Stoll]

OK; maybe I should get acquainted with aesop better. Somehow my mental model is that it rarely works and is slow...

[Jireh Loreaux]

Also, I'm slightly confused about how you end up with a coercion on the 1. Isn't it already of type ℂ in the lemma?

[Jireh Loreaux]

(I have to teach, so need to stop responding now.)

[Michael Stoll]

In the more general lemma, x is a real number, so you apply it to a real 1.

[Michael Stoll]

(I have to cook dinner now.)

[Yury G. Kudryashov]

positivity can prove ≠ 0 but it assumes PartialOrder everywhere.

[Yury G. Kudryashov]

Michael Stoll said:

What would be a good file for the following to go in?

lemma Complex.indicator_ofReal {f : ℕ → ℝ} {s : Set ℕ} :
    (fun n ↦ ((Set.indicator s f n : ℝ) : ℂ)) = Set.indicator s (fun n ↦ (f n : ℂ))

#find_home suggests Mathlib.Data.Complex.Abs, Mathlib.Data.Complex.Cardinality, Mathlib.Data.Complex.BigOperators, none of which looks very convincing.

What's your proof? Why do you need Nat here? Is it just docs#Set.indicator_comp_of_zero ?

[Michael Stoll]

I think, aesop in this case basically just runs simp, BTW. (In fact, the shortest proof is probably by simp [hy],
which I'm now using in my code.)

[Jireh Loreaux]

perfect

[Michael Stoll]

Yury G. Kudryashov said:

Michael Stoll said:

What would be a good file for the following to go in?

lemma Complex.indicator_ofReal {f : ℕ → ℝ} {s : Set ℕ} :
    (fun n ↦ ((Set.indicator s f n : ℝ) : ℂ)) = Set.indicator s (fun n ↦ (f n : ℂ))

#find_home suggests Mathlib.Data.Complex.Abs, Mathlib.Data.Complex.Cardinality, Mathlib.Data.Complex.BigOperators, none of which looks very convincing.

What's your proof? Why do you need Nat here? Is it just docs#Set.indicator_comp_of_zero ?

In my use case, it's about Nat. But you are right that it follows easily from docs#Set.indicator_comp_of_zero .
It is sometimes hard to guess the level of generality of a result in Mathlib. Here, apply? does not find this lemma (with or without preceding ext), and aesop fails. (My proof is basically ext n; by_cases h : n ∈ s <;> simp [h].)

[Michael Stoll]

Another question: Would it make sense to add these?

lemma Complex.summable_re {α : Type u_1} {f : α → ℂ} (h : Summable f) : Summable fun x ↦ (f x).re :=
  (Complex.hasSum_re h.hasSum).summable

lemma Complex.summable_im {α : Type u_1} {f : α → ℂ} (h : Summable f) : Summable fun x ↦ (f x).im :=
  (Complex.hasSum_im h.hasSum).summable

The proofs are short, but the statements are sometimes convenient (and there are many similar cases where there are HasSum and Summable versions).

[Jireh Loreaux]

One thing I did notice about your statement (aside from the ℕ issue). So in order to understand it, I had to reconfigure it in my head to (↑) ∘ (Set.indicator s f) = Set.indicator s ((↑) ∘ f), which was a bit cleaner. But I didn't have time to go looking for the lemma.

This version exact?finds without trouble.

import Mathlib

lemma Complex.indicator_ofReal {f : ℕ → ℝ} {s : Set ℕ} :
    ((↑) : ℝ → ℂ) ∘ Set.indicator s f = Set.indicator s ((↑) ∘ f) := by
  exact? -- exact (Set.indicator_comp_of_zero rfl).symm

So, in this case, finding the cleanest phrasing was the problem, not so much the level of generality.

[Kevin Buzzard]

Michael Stoll said:

In the more general lemma, x is a real number, so you apply it to a real 1.

In the more general lemma I called the new variable z precisely because I thought it should be a complex number.

[Michael Stoll]

OK; I guess that would work. (But it's a moot point by now...)