AEStronglyMeasurable of composition with innerSL

Stream: Is there code for X?

[Alex Kontorovich]

I can't seem to find any good API to handle something like the below, an AEStronglyMeasurable function f turned into a continuous linear map by toSpanSingleton, composed with innerSL. It should just be a chain of continuities on top of hf_AE, right?... Any help here would be much appreciated, thanks!

import Mathlib.Topology.Algebra.Module.Basic
import Mathlib.Analysis.InnerProductSpace.Basic
import Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
import Mathlib.MeasureTheory.Function.L1Space

open MeasureTheory

example (E : Type*) (F : Type*) [inst : NormedAddCommGroup E]
  [InnerProductSpace ℝ E] [MeasureSpace E] [BorelSpace E] [FiniteDimensional ℝ E]
  [NormedAddCommGroup F] [inst_6 : NormedSpace ℂ F] [inst_7 : CompleteSpace F] {f : E → F}
  (hf_AE : AEStronglyMeasurable f volume) :
  AEStronglyMeasurable
    (fun w ↦ ContinuousLinearMap.comp (ContinuousLinearMap.toSpanSingleton ℝ (f w))
    ((innerSL ℝ) w)) volume := by
  sorry

[Alex Kontorovich]

Paging @Sébastien Gouëzel @Yury G. Kudryashov in case you can help here? (FYI This is the last remaining step in a project with @Heather Macbeth to compute the derivative of the Fourier transform. The latter itself is a step towards showing that the Fourier transform of a Schwartz function is also Schwartz...)

[Yury G. Kudryashov]

What's the codomain of the new function?

[Yury G. Kudryashov]

I see. Working on it.

[Yury G. Kudryashov]

  refine (ContinuousLinearMap.compL ℝ E ℝ F).aestronglyMeasurable_comp₂ ?_ ?_
  · refine Continuous.comp_aestronglyMeasurable ?_ hf_AE
    sorry
  · exact (innerSL ℝ).continuous.aestronglyMeasurable

leaves a sorry saying that toSpanSingleton is continuous. Please add a LinearIsometry version of this map using docs#ContinuousLinearMap.norm_toSpanSingleton

[Yury G. Kudryashov]

Here is a sorry-free version:

  refine (ContinuousLinearMap.compL ℝ E ℝ F).aestronglyMeasurable_comp₂ ?_ ?_
  · refine Continuous.comp_aestronglyMeasurable ?_ hf_AE
    exact (ContinuousLinearMap.smulRightL ℝ ℝ F 1).continuous
  · exact (innerSL ℝ).continuous.aestronglyMeasurable

[Alex Kontorovich]

Amazing thank you!!!