`BookProof.HalfLineLimitCircle.inner_eq_integral` {u v : HL} {a b : ℝ → ℂ} (hu : (u : ℝ → ℂ) =ᵐ[hlMeasure] a) (hv : (v : ℝ → ℂ) =ᵐ[hlMeasure] b) : (inner ℂ u v : ℂ) =...

Initializing...

`BookProof.HalfLineLimitCircle.inner_eq_integral` {u v : HL} {a b : ℝ → ℂ} (hu : (u : ℝ → ℂ) =ᵐ[hlMeasure] a) (hv : (v : ℝ → ℂ) =ᵐ[hlMeasure] b) : (inner ℂ u v : ℂ) =... · Prove2Me