noncomputable def FourierTransformMeasure.fourierTransformMeasure (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasure μ] (ξ : ℝ) : ℂ

theorem FourierTransformMeasure.continuous_fourierTransformMeasure {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsFiniteMeasure μ] : Continuous (fourierTransformMeasure μ)

theorem FourierTransformMeasure.norm_fourierTransformMeasure_le {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsFiniteMeasure μ] (ξ : ℝ) : ‖fourierTransformMeasure μ ξ‖ ≤ μ.real Set.univ

noncomputable def FourierTransformMeasure.fourierTransformBCF (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasure μ] : BoundedContinuousFunction ℝ ℂ

@[simp]

theorem FourierTransformMeasure.fourierTransformBCF_apply {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsFiniteMeasure μ] (ξ : ℝ) : (fourierTransformBCF μ) ξ = fourierTransformMeasure μ ξ

theorem FourierTransformMeasure.eq_of_fourierTransformMeasure_eq {μ ν : MeasureTheory.Measure ℝ} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (h : fourierTransformMeasure μ = fourierTransformMeasure ν) : μ = ν

noncomputable def FourierTransformMeasure.schwartzFourierTransform (φ : SchwartzMap ℝ ℂ) : ℝ → ℂ

theorem FourierTransformMeasure.parseval_fubini_measure (μ : MeasureTheory.Measure ℝ) (hμ : MeasureTheory.IsFiniteMeasure μ) (φ : SchwartzMap ℝ ℂ) : ∫ (ξ : ℝ), φ ξ * fourierTransformMeasure μ ξ = ∫ (y : ℝ), schwartzFourierTransform φ y ∂μ

noncomputable def FourierTransformMeasure.mulEquiv (c : ℝ) (hc : c ≠ 0) : ℝ ≃L[ℝ] ℝ

@[simp]

theorem FourierTransformMeasure.mulEquiv_apply (c : ℝ) (hc : c ≠ 0) (x : ℝ) : (mulEquiv c hc) x = c * x

theorem FourierTransformMeasure.sft_eq_fourier_at (φ : SchwartzMap ℝ ℂ) (y : ℝ) : schwartzFourierTransform φ y = FourierTransform.fourier (⇑φ) (y / (2 * Real.pi))

theorem FourierTransformMeasure.fourier_surjective_schwartz (f : SchwartzMap ℝ ℂ) : ∃ (φ : SchwartzMap ℝ ℂ), ∀ (y : ℝ), schwartzFourierTransform φ y = f y

theorem FourierTransformMeasure.exists_norm_le_of_tendsto {f : ℕ → ℂ} {L : ℂ} (hf : Filter.Tendsto f Filter.atTop (nhds L)) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (j : ℕ), ‖f j‖ ≤ C

theorem FourierTransformMeasure.measureReal_eq_norm_charFun_zero (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasure μ] : μ.real Set.univ = ‖MeasureTheory.charFun μ 0‖

theorem FourierTransformMeasure.schwartz_weak_convergence_of_fourierTransform_tendsto (μseq : ℕ → MeasureTheory.Measure ℝ) [∀ (j : ℕ), MeasureTheory.IsFiniteMeasure (μseq j)] (ν : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasure ν] (hconv : ∀ (ξ : ℝ), Filter.Tendsto (fun (j : ℕ) => fourierTransformMeasure (μseq j) ξ) Filter.atTop (nhds (fourierTransformMeasure ν ξ))) (f : SchwartzMap ℝ ℂ) : Filter.Tendsto (fun (j : ℕ) => ∫ (x : ℝ), f x ∂μseq j) Filter.atTop (nhds (∫ (x : ℝ), f x ∂ν))

def WeakConvergencePortmanteau.WeakConvergenceSmooth (μseq : ℕ → MeasureTheory.Measure ℝ) (μ : MeasureTheory.Measure ℝ) : Prop

theorem WeakConvergencePortmanteau.exists_smooth_bump_upper (a b : ℝ) (hab : a < b) (ε : ℝ) (hε : 0 < ε) : ∃ (f : ℝ → ℝ), (∀ (n : ℕ), ContDiff ℝ (↑n) f) ∧ HasCompactSupport f ∧ (∀ (x : ℝ), 0 ≤ f x) ∧ (∀ (x : ℝ), f x ≤ 1) ∧ (∀ x ∈ Set.Icc a b, f x = 1) ∧ ∀ (x : ℝ), f x ≠ 0 → x ∈ Set.Ioo (a - ε) (b + ε)

theorem WeakConvergencePortmanteau.exists_smooth_bump_lower (a b ε : ℝ) (hε : 0 < ε) (hε_small : ε < (b - a) / 2) : ∃ (f : ℝ → ℝ), (∀ (n : ℕ), ContDiff ℝ (↑n) f) ∧ HasCompactSupport f ∧ (∀ (x : ℝ), 0 ≤ f x) ∧ (∀ (x : ℝ), f x ≤ 1) ∧ (∀ x ∈ Set.Icc (a + ε) (b - ε), f x = 1) ∧ ∀ (x : ℝ), f x ≠ 0 → x ∈ Set.Ioo a b

theorem WeakConvergencePortmanteau.measure_le_ofReal_integral {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsFiniteMeasure μ] {S : Set ℝ} (hS : MeasurableSet S) {f : ℝ → ℝ} (hf_nn : ∀ (x : ℝ), 0 ≤ f x) (hf_one : ∀ x ∈ S, 1 ≤ f x) (hf_int : MeasureTheory.Integrable f μ) : μ S ≤ ENNReal.ofReal (∫ (x : ℝ), f x ∂μ)

theorem WeakConvergencePortmanteau.ofReal_integral_le_measure {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsFiniteMeasure μ] {T : Set ℝ} (hT : MeasurableSet T) {f : ℝ → ℝ} (hf_nn : ∀ (x : ℝ), 0 ≤ f x) (hf_le : ∀ (x : ℝ), f x ≤ 1) (hf_supp : ∀ (x : ℝ), f x ≠ 0 → x ∈ T) (hf_int : MeasureTheory.Integrable f μ) : ENNReal.ofReal (∫ (x : ℝ), f x ∂μ) ≤ μ T

theorem WeakConvergencePortmanteau.limsup_measure_Ioo_le_of_weakConvergence (μseq : ℕ → MeasureTheory.Measure ℝ) [∀ (j : ℕ), MeasureTheory.IsFiniteMeasure (μseq j)] (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasure μ] (hweak : WeakConvergenceSmooth μseq μ) {a b : ℝ} (hab : a < b) {ε : ℝ} (hε : 0 < ε) : Filter.limsup (fun (j : ℕ) => (μseq j) (Set.Ioo a b)) Filter.atTop ≤ μ (Set.Ioo (a - ε) (b + ε))

theorem WeakConvergencePortmanteau.measure_Ioo_le_liminf_of_weakConvergence (μseq : ℕ → MeasureTheory.Measure ℝ) [∀ (j : ℕ), MeasureTheory.IsFiniteMeasure (μseq j)] (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasure μ] (hweak : WeakConvergenceSmooth μseq μ) {a b ε : ℝ} (hε : 0 < ε) (hε_small : ε < (b - a) / 2) : μ (Set.Ioo (a + ε) (b - ε)) ≤ Filter.liminf (fun (j : ℕ) => (μseq j) (Set.Ioo a b)) Filter.atTop

theorem WeakConvergencePortmanteau.limsup_measure_Ioo_le_measure_Icc (μseq : ℕ → MeasureTheory.Measure ℝ) [∀ (j : ℕ), MeasureTheory.IsFiniteMeasure (μseq j)] (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasure μ] (hweak : WeakConvergenceSmooth μseq μ) {a b : ℝ} (hab : a < b) : Filter.limsup (fun (j : ℕ) => (μseq j) (Set.Ioo a b)) Filter.atTop ≤ μ (Set.Icc a b)

theorem WeakConvergencePortmanteau.measure_Ioo_le_liminf_measure_Ioo (μseq : ℕ → MeasureTheory.Measure ℝ) [∀ (j : ℕ), MeasureTheory.IsFiniteMeasure (μseq j)] (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasure μ] (hweak : WeakConvergenceSmooth μseq μ) {a b : ℝ} (_hab : a < b) : μ (Set.Ioo a b) ≤ Filter.liminf (fun (j : ℕ) => (μseq j) (Set.Ioo a b)) Filter.atTop

theorem WeakConvergencePortmanteau.tendsto_measure_Ioo_of_no_atoms (μseq : ℕ → MeasureTheory.Measure ℝ) [∀ (j : ℕ), MeasureTheory.IsFiniteMeasure (μseq j)] (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasure μ] (hweak : WeakConvergenceSmooth μseq μ) {a b : ℝ} (hab : a < b) (ha : μ {a} = 0) (hb : μ {b} = 0) : Filter.Tendsto (fun (j : ℕ) => (μseq j) (Set.Ioo a b)) Filter.atTop (nhds (μ (Set.Ioo a b)))