How to prove that a parametric integral is continuous

Stream: mathlib4

[Jeremy Tan]

I have the following improper integral (Landen's integral, related to the AGM which I introduce in #32892) and I would like to prove that it is continuous in its two parameters a, b when both are positive.

import Mathlib.Analysis.SpecialFunctions.ImproperIntegrals

open MeasureTheory Topology Real

/-- The elliptic integral related to the arithmetic-geometric mean. -/
noncomputable def agmIntegral (a b : ℝ) : ℝ :=
  ∫ x in Set.Ioi 0, (√((x ^ 2 + a ^ 2) * (x ^ 2 + b ^ 2)))⁻¹

variable {a b : ℝ}

lemma continuousOn_agmIntegral :
    ContinuousOn (fun p ↦ agmIntegral p.1 p.2) (Set.Ioi 0 ×ˢ Set.Ioi 0) := by
  sorry

I can't see a simple way of proving it. It's improper, so continuousOn_integral_of_compact_support doesn't work here. How can I do it?

[Yongxi Lin (Aaron)]

I guess you can apply continuousOn_integral_of_compact_supporton each compact neighborhood. You probably should first prove a local version of continuousOn_integral_of_compact_support.

[Jeremy Tan]

There is also docs#MeasureTheory.continuousWithinAt_of_dominated but I am not sure whether it can be applied, and if so how to apply it

[Jeremy Tan]

I could for example transform the integral to the trigonometric form (closer to Legendre's elliptic integrals, over 0..π / 2) and then apply continuousOn_integral_of_compact_support, but that approach feels too long-winded

[Jeremy Tan]

Found a way to do it without passing to the trigonometric form. The completed PR is #34397