Porting Analysis.Fourier.PoissonSummation

Stream: mathlib4

[David Loeffler]

Hi folks,

I'm trying to port the file Analysis.Fourier.PoissonSummation. The error I'm currently stuck at is the following.

theorem Real.fourierCoeff_tsum_comp_add {f : C(ℝ, ℂ)}
    (hf : ∀ K : Compacts ℝ, Summable fun n : ℤ => ‖(f.comp (ContinuousMap.addRight n)).restrict K‖)
    (m : ℤ) : fourierCoeff (Periodic.lift <| f.periodic_tsum_comp_add_zsmul 1) m = 𝓕 f m := by
  let e : C(ℝ, ℂ) := (fourier (-m)).comp ⟨(coe : ℝ → UnitAddCircle), continuous_quotient_mk'⟩
  [...]

There's no error reported here (it generates a weird error further down the same proof), but something goes wrong already at this step, because the tactic state view shows

e: C(ℝ, ℂ) := ContinuousMap.comp (fourier (-m)) (ContinuousMap.mk (sorryAx (ℝ → UnitAddCircle) true))

and the sorryAx clearly isn't what's meant to happen. Any thoughts what might be going on?

[Matthew Ballard]

Do you need to replace coe with (↑)?

[David Loeffler]

OK, that worked, but unfortunately it doesn't solve the weird error a few lines further down as I'd hoped it would :-(

[David Loeffler]

A few lines later I have

simp_rw [ContinuousMap.comp_apply, mul_comp] at eadd ⊢

where eadd is some hypothesis in the context. It puts a red underline under at, with the error message expected ':='. Why would it expect that?

[Ruben Van de Velde]

We're gonna need more context for this one

[Ruben Van de Velde]

Do you have this up in a PR?

[Kevin Buzzard]

Probably unrelated but the first thing I do when I don't understand what's going on is set_option autoImplicit false at the top of the file.

[David Loeffler]

This is !4#5306.
@Kevin Buzzard Thanks for the suggestion but it doesn't seem to help here.

[Kevin Buzzard]

If you comment out the suffices on line 97 then you get some less inscrutible errors.

[Ruben Van de Velde]

Yeah, it's the := in suffices; I pushed a small fix

[Ruben Van de Velde]

That's an interesting failure mode, and a terrible error message

[Moritz Doll]

is this a bug in mathport?

[Kevin Buzzard]

mathport didn't put the := there. I have been caught out by this change in the syntax of suffices at least once before.

[David Loeffler]

OK, thanks everyone! I'm sure I'll be back again soon enough (when I hit the next failure)

[Kevin Buzzard]

If you delete the := then the line is suffices foo : integrable ⇑(e * f); exact this.has_sum_interval_integral_comp_add_int.tsum_eq and there's an error on ; saying "expected :=" which, if this isn't valid syntax any more, is an even more terrible error message!

[Kevin Buzzard]

@David Loeffler got it: remove the ⇑ after integrable.

[Ruben Van de Velde]

Mathport output was

      suffices : integrable ⇑(e * f); exact this.has_sum_interval_integral_comp_add_int.tsum_eq

fwiw

[Kevin Buzzard]

yeah so it's the up-arrow which needs to be removed.

[David Loeffler]

Here's an annoying regression: in mathlib3 I could write ∫ x in 0..1, f x and it would recognise it as an interval integral; here it seems I need to specify the type explicitly as ∫ x in (0:ℝ)..1, f x.

[David Loeffler]

I've been working on this while waiting at Birmingham airport for a delayed flight. The good news is that the PR is now ready for review. The bad news is that my flight just got cancelled :frown: