PRs from APAP

Stream: PR reviews

[Yaël Dillies]

The PRs from my Arithmetic Progressions - Almost Periodicity project are starting to pile up. Could I get some reviews/merges, please? The full list is here and here is a more detailed description of the important PRs:

[Yaël Dillies]

• #15441 feat(AddChar): Additive group structure and double dual embedding: Provide the additive group structure on AddChar G ℂ (it equals the multiplicative group structure, which already exists, but that's necessary for AddChar (AddChar G ℂ) ℂ to make sense), then define the double dual embedding as a map G → AddChar (AddChar G ℂ) ℂ. Approved on principles by @Bhavik Mehta, @Michael Stoll, @David Loeffler.

[Yaël Dillies]

• #15443 feat: The Marcinkiewicz-Zygmund inequality: Prove the Marcinkiewicz-Zygmund inequality for a uniform random variable indexed by a fintype. Golfed by @Heather Macbeth and reviewed by @Sébastien Gouëzel. This was partly written by Bhavik.

[Yaël Dillies]

• #15883 feat: Expectation of a function over a finset: Define the expectation of a random variable over a finset. This is a special case of the barycenter in a convex space. However this generality depends on a huge refactor I am currently preparing. Approved by @Bhavik Mehta, reviewed by @Eric Wieser and @Daniel Weber. This was partly written by Bhavik.

[Yaël Dillies]

• #16181 feat: Conjugation-negation operator: Define the conjugation-negation conjneg f of a function f as fun x ↦ conj f (-x). This is an important operator in Fourier analysis as convolution by f is adjoint to convolution by conjneg f: ⟨f ∗ g, h⟩ = ⟨g, conjneg f ∗ h⟩. Reviewed by @Eric Wieser, @Bhavik Mehta.

[Yaël Dillies]

• #16183 feat: The translation operator: Define the translation τ a f of a function f by an element a of the domain. This is "just" DomMulAct.mk (-a) • f but it seems tough to make τ a fnotation for it as then τ (-a) f would get "simplified" to DomMulAct.mk a • f. One option would be to depart from mathematical convention by making τ a f be notation for DomMulAct.mk a • f. It would work fine for my application but it might be unexpected to people for τ a f a to be f (2 • a) rather than f 0. Approved by @Bhavik Mehta, reviewed by @Eric Wieser.

[Yaël Dillies]

Note that, even though Bhavik was not involved in all of the above PRs, he is involved enough in the underlying project that we would like someone else to sign off the above PRs.

[Yaël Dillies]

So far one PR merged and one reviewed. Thanks! Here's one more:

[Yaël Dillies]

• #16447 feat: L2 inner product of finite sequences: Define the discrete L2 inner product of functions f g : ι → R where ι is a fintype as ∑ i, conj (f i) * g i. This "duplicates" inner but is necessary for two reasons:

  1. It does not need the codomain to be RCLike, notably allowing its use for NNReal-valued functions.
  2. This is the inner product in the discrete normalisation. A future PR will add a similar API for the "compact" one.

[Eric Wieser]

1) feels like it is revealing the existence of a rather larger can of worms

[Kim Morrison]

Perhaps Eric is suggesting that it would be good to indicate how this is going to be used later? Understanding just how big the can is might be a prerequisite for reviewing #16447.

[Yaël Dillies]

APAP is freely available online. Searching through, you can find all uses of the new notation and indeed all of them are either on a generic type or ℝ or ℂ, so I would be happy with the RCLike generality.

[Yaël Dillies]

Let me therefore replace point 1) above by

3. I keep on manipulating functions G → K (where G is a finite abelian group) in different norms, so I don't want to be dealing with type synonyms all the time.
4. The design of having operations on the original type which can be interpreted as some algebraic or metric structure on a type synonym already exists, eg docs#MeasureTheory.eLpNorm vs ‖_‖.

[Bhavik Mehta]

My take on the inner product stuff is that we do need duplication somewhere, and having an inner product defined for functions indexed by a finite type is valuable (in the same way we have finite sums as well as integrals, despite the former being a special case of the latter). But I'm not convinced that we need three different versions depending on the choice of normalisation: I think we should give an inner product parametrised by a weighting function (I believe this part is already planned), then the discrete+compact normalisations can be abbreviations of this.

[Jireh Loreaux]

Yes, this seems like an appropriate solution to me.

[Yaël Dillies]

@Heather Macbeth, @Sébastien Gouëzel, any more thoughts on #15443 ?

[Yaël Dillies]

:ping_pong: @Sébastien Gouëzel