Integrability of a function with support in a compact set

Stream: Is there code for X?

[Vláďa Sedláček]

If F : ℝ × ℝ → ℂ is a function with continuousOn F S and F_supp: F.support ⊆ S, where ST : S ⊆ T and T_comp : IsCompact T (in fact, in my use case, S is open and T is its closure), is there a good way to conclude that Integrable F? Using

refine (integrableOn_iff_integrable_of_support_subset F_supp).mp ?_

reduces this to Integrable F S (and I'm not sure how to proceed), while

refine (integrableOn_iff_integrable_of_support_subset <| subset_trans F_supp ST).mp ?_
refine ContinuousOn.integrableOn_compact T_comp ?_

reduces it to ContinuousOn F T (and I think this might be false in general). Am I missing something?

[Sébastien Gouëzel]

What about F x = 1/x if x is in S = (0, 1) and 0 elsewhere? It is continuous on S, zero outside, and yet it is not integrable.

[Vláďa Sedláček]

Ah I see, then I abstracted away too much. So how about this particular case?

import Mathlib.MeasureTheory.Integral.IntegralEqImproper
open Set MeasureTheory

noncomputable def DeltaSpike (Ψ : ℝ → ℝ) (ε : ℝ) : ℝ → ℝ :=
  fun x => Ψ (x ^ (1 / ε)) / ε

example (Ψ : ℝ → ℝ) (suppΨ : Ψ.support ⊆ Icc (1 / 2) 2) (diffΨ : ContDiff ℝ 1 Ψ)
    {ε : ℝ} (εpos : 0 < ε)
    {s : ℂ} (hs : 0 < s.re)
    (f : ℝ → ℂ := fun x ↦ DeltaSpike Ψ ε x)
    (g : ℝ → ℂ := fun x ↦ if 0 < x ∧ x ≤ 1 then 1 else 0)
    (F : ℝ × ℝ → ℂ := Function.uncurry fun x y ↦ f y * g (x / y) / (y : ℂ) * (x : ℂ) ^ (s - 1)) :
    IntegrableOn F (Ioi 0 ×ˢ Ioi 0) := by
  let S := Ioc 0 ((2 : ℝ) ^ ε) ×ˢ Icc ((2 : ℝ) ^ (-ε)) ((2 : ℝ) ^ ε)
  let T := Icc 0 ((2 : ℝ) ^ ε) ×ˢ Icc ((2 : ℝ) ^ (-ε)) ((2 : ℝ) ^ ε)
  have T_comp : IsCompact T := IsCompact.prod isCompact_Icc isCompact_Icc
  have F_supp : F.support ⊆ S := by sorry -- this is not hard to show
  refine (integrableOn_iff_integrable_of_support_subset F_supp).mp ?_
  sorry

[Floris van Doorn]

Not your question, but note that (f : ℝ → ℂ := fun x ↦ DeltaSpike Ψ ε x) is not the same as
let f : ℝ → ℂ := fun x ↦ DeltaSpike Ψ ε x, and you probably mean the latter.

[Vláďa Sedláček]

I believe that the key is that F is bounded in y and integrable in x, so MeasureTheory.integrable_prod_iff could be used; I'm not sure how to prove its assumption AEStronglyMeasurable F (Measure.prod volume volume) though.