`BookProof.RadialMollifier.polar_radial` {δ : ℝ} (hδ : 0 < δ) (G : ℂ → ℂ) (hG : Continuous G) : ∫ u : ℂ, (moll δ u : ℂ) * G u = ∫ r in Ioi (0 : ℝ), ((r * moll δ r : ℝ)...

Proved

BookProof.RadialMollifier.polar_radial

by leonardopedro · Oct 10, 2026 · Mathlib 0df444a (Lean v4.33.1)

theoremstimepiece

Prove the following Lean 4 theorem from ChapterRadialMollifier.

BookProof.RadialMollifier.polar_radial {δ : ℝ} (hδ : 0 < δ) (G : ℂ → ℂ) (hG : Continuous G) : ∫ u : ℂ, (moll δ u : ℂ) * G u = ∫ r in Ioi (0 : ℝ), ((r * moll δ r : ℝ) : ℂ) * ∫ θ in (-π)..π, G (Complex.polarCoord.symm (r, θ))

Formalization note: Lean 4 identifier BookProof.RadialMollifier.polar_radial.

Preamble

-- Generated from ChapterRadialMollifier.lean — theorem BookProof.RadialMollifier.polar_radial
import Mathlib
import Definitions.Def_ChapterRadialMollifier
open BookProof.RadialMollifier



open MeasureTheory Metric Set Complex intervalIntegral Real
open scoped Convolution Topology ContDiff Real

noncomputable section

Formal statement

theorem BookProof.RadialMollifier.polar_radial {δ : ℝ} (hδ : 0 < δ) (G : ℂ → ℂ) (hG : Continuous G) :
    ∫ u : ℂ, (moll δ u : ℂ) * G u
      = ∫ r in Ioi (0 : ℝ), ((r * moll δ r : ℝ) : ℂ) *
          ∫ θ in (-π)..π, G (Complex.polarCoord.symm (r, θ)) := by sorry

View graph