theorem Frourio.lintegral_union_disjoint {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) {s t : Set α} (hs : MeasurableSet s) (ht : MeasurableSet t) (hst : Disjoint s t) (f : α → ENNReal) (hf : Measurable f) : ∫⁻ (x : α) in s ∪ t, f x ∂μ = ∫⁻ (x : α) in s, f x ∂μ + ∫⁻ (x : α) in t, f x ∂μ

Manual construction of lintegral_union for disjoint sets

theorem Frourio.schwartz_finite_on_unit_interval {σ : ℝ} (hσ : 1 / 2 < σ) (f : SchwartzMap ℝ ℂ) : (∫⁻ (x : ℝ) in Set.Ioc 0 1, ‖f x‖ₑ ^ 2 ∂mulHaar.withDensity fun (x : ℝ) => ENNReal.ofReal (x ^ (2 * σ - 1))) < ⊤

Schwartz functions have finite weighted L² norm on (0,1] for σ > 1/2

theorem Frourio.schwartz_finite_on_tail {σ : ℝ} (f : SchwartzMap ℝ ℂ) : (∫⁻ (x : ℝ) in Set.Ioi 1, ‖f x‖ₑ ^ 2 ∂mulHaar.withDensity fun (x : ℝ) => ENNReal.ofReal (x ^ (2 * σ - 1))) < ⊤

Schwartz functions have finite weighted L² norm on (1,∞) for any σ

theorem Frourio.schwartz_mem_Hσ {σ : ℝ} (hσ : 1 / 2 < σ) (f : SchwartzMap ℝ ℂ) : MeasureTheory.MemLp (fun (x : ℝ) => if x > 0 then f x else 0) 2 (mulHaar.withDensity fun (x : ℝ) => ENNReal.ofReal (x ^ (2 * σ - 1)))

Schwartz functions restricted to (0,∞) belong to Hσ for σ > 1/2

noncomputable def Frourio.schwartzToHσ {σ : ℝ} (hσ : 1 / 2 < σ) (f : SchwartzMap ℝ ℂ) : ↥(Hσ σ)

The embedding of Schwartz functions into Hσ for σ > 1/2

Equations

• Frourio.schwartzToHσ hσ f = MeasureTheory.MemLp.toLp (fun (x : ℝ) => if x > 0 then f x else 0) ⋯

theorem Frourio.schwartzToHσ_linear {σ : ℝ} (hσ : 1 / 2 < σ) (a : ℂ) (f g : SchwartzMap ℝ ℂ) : schwartzToHσ hσ (a • f + g) = a • schwartzToHσ hσ f + schwartzToHσ hσ g

The embedding is linear for σ > 1/2

theorem Frourio.norm_toLp_eq_toReal_eLpNorm {σ : ℝ} (hσ : 1 / 2 < σ) (f : SchwartzMap ℝ ℂ) : ‖MeasureTheory.MemLp.toLp (fun (x : ℝ) => if x > 0 then f x else 0) ⋯‖ = (MeasureTheory.eLpNorm (fun (x : ℝ) => if x > 0 then f x else 0) 2 (mulHaar.withDensity fun (x : ℝ) => ENNReal.ofReal (x ^ (2 * σ - 1)))).toReal

The norm of the toLp embedding equals the ENNReal.toReal of the eLpNorm

theorem Frourio.schwartzToHσ_ae_eq {σ : ℝ} (hσ : 1 / 2 < σ) (φ : SchwartzMap ℝ ℂ) : ↑↑(schwartzToHσ hσ φ) =ᵐ[mulHaar.withDensity fun (x : ℝ) => ENNReal.ofReal (x ^ (2 * σ - 1))] fun (x : ℝ) => if x > 0 then φ x else 0

For any f ∈ Hσ, schwartzToHσ hσ φ and the truncated φ agree a.e. for σ > 1/2

theorem Frourio.eLpNorm_bound_on_tail {σ : ℝ} {k₁ : ℕ} (hσk : σ + 1 / 2 ≤ ↑k₁) (f : SchwartzMap ℝ ℂ) : MeasureTheory.eLpNorm (fun (x : ℝ) => if x ∈ Set.Ioi 1 then f x else 0) 2 (mulHaar.withDensity fun (x : ℝ) => ENNReal.ofReal (x ^ (2 * σ - 1))) ≤ ENNReal.ofReal ((SchwartzMap.seminorm ℝ k₁ 0) f * √(1 / (2 * ↑k₁ - 2 * σ)))

theorem Frourio.eLpNorm_bound_on_unit_interval {σ : ℝ} (f : SchwartzMap ℝ ℂ) (M : ℝ) (hM_bound : (∫⁻ (x : ℝ) in Set.Ioc 0 1, ENNReal.ofReal (x ^ (2 * σ - 1)) ∂mulHaar) ^ (1 / 2) ≤ ENNReal.ofReal M) : MeasureTheory.eLpNorm (fun (x : ℝ) => if x ∈ Set.Ioc 0 1 then f x else 0) 2 (mulHaar.withDensity fun (x : ℝ) => ENNReal.ofReal (x ^ (2 * σ - 1))) ≤ ENNReal.ofReal ((SchwartzMap.seminorm ℝ 0 0) f * M)

Bound for the eLpNorm of a Schwartz function on the unit interval (0,1]

theorem Frourio.eLpNorm_split_at_one {σ : ℝ} (f : SchwartzMap ℝ ℂ) : MeasureTheory.eLpNorm (fun (x : ℝ) => if x > 0 then f x else 0) 2 (mulHaar.withDensity fun (x : ℝ) => ENNReal.ofReal (x ^ (2 * σ - 1))) ≤ MeasureTheory.eLpNorm (fun (x : ℝ) => if x ∈ Set.Ioc 0 1 then f x else 0) 2 (mulHaar.withDensity fun (x : ℝ) => ENNReal.ofReal (x ^ (2 * σ - 1))) + MeasureTheory.eLpNorm (fun (x : ℝ) => if x ∈ Set.Ioi 1 then f x else 0) 2 (mulHaar.withDensity fun (x : ℝ) => ENNReal.ofReal (x ^ (2 * σ - 1)))

Splitting the eLpNorm of a function on (0,∞) into (0,1] and (1,∞) parts

theorem Frourio.weight_function_L2_bound_unit {σ : ℝ} (hσ : 1 / 2 < σ) : ∃ (M : ℝ), 0 < M ∧ (∫⁻ (x : ℝ) in Set.Ioc 0 1, ENNReal.ofReal (x ^ (2 * σ - 1)) ∂mulHaar) ^ (1 / 2) ≤ ENNReal.ofReal M

The weight function has finite L² norm on (0,1] for σ > 1/2

theorem Frourio.mulHaar_measure_Icc_lt_top {a b : ℝ} (ha : 0 < a) : a ≤ b → mulHaar (Set.Icc a b) < ⊤

Finiteness of the mulHaar measure on a positive closed interval.

theorem Frourio.weight_integrableOn_Icc {σ a b : ℝ} (ha : 0 < a) (hab : a ≤ b) : MeasureTheory.IntegrableOn (fun (x : ℝ) => x ^ (2 * σ - 1)) (Set.Icc a b) mulHaar

Integrability of the weight x^(2σ-1) on a positive closed interval with respect to mulHaar.

theorem Frourio.weight_locallyIntegrable {σ : ℝ} : 1 / 2 < σ → MeasureTheory.LocallyIntegrableOn (fun (x : ℝ) => x ^ (2 * σ - 1)) (Set.Ioi 0) mulHaar

The weight function x^(2σ-1) is locally integrable on (0,∞) for σ > 1/2

theorem Frourio.memLp_of_Hσ {σ : ℝ} (f : ↥(Hσ σ)) : MeasureTheory.MemLp (Hσ.toFun f) 2 (mulHaar.withDensity fun (x : ℝ) => ENNReal.ofReal (x ^ (2 * σ - 1)))

Elements of Hσ σ lie in the defining weighted L² space.

theorem Frourio.simpleFunc_bounded_support_integrable (f : MeasureTheory.SimpleFunc ℝ ℂ) (R : ℝ) : 0 < R → ∀ (hR_bound : Function.support ⇑f ⊆ Set.Icc (-R) R), MeasureTheory.Integrable (⇑f) MeasureTheory.volume

Simple functions with bounded support are integrable in Lebesgue measure

theorem Frourio.finite_support_bounded (f : ℝ → ℂ) (hf_finite : (Function.support f).Finite) : ∃ (R : ℝ), 0 < R ∧ Function.support f ⊆ Metric.closedBall 0 R

Simple functions with finite support have bounded support

theorem Frourio.range_norm_subset_tsupport_image_with_zero (φ : ℝ → ℝ) : (Set.range fun (x : ℝ) => ‖φ x‖) ⊆ Set.insert 0 ((fun (x : ℝ) => ‖φ x‖) '' tsupport φ)

theorem Frourio.continuous_convolution_integrable_smooth (f : ℝ → ℂ) (φ : ℝ → ℝ) (hf_integrable : MeasureTheory.Integrable f MeasureTheory.volume) (hφ_smooth : ContDiff ℝ (↑⊤) φ) (hφ_compact : HasCompactSupport φ) : Continuous fun (x : ℝ) => ∫ (y : ℝ), f y * ↑(φ (x - y))

Convolution of integrable function with smooth compact support function is continuous

theorem Frourio.simpleFunc_truncation_integrable {σ : ℝ} : 1 / 2 < σ → ∀ (f : MeasureTheory.SimpleFunc ℝ ℂ) (R : ℝ), MeasureTheory.Integrable (fun (x : ℝ) => if |x| ≤ R then f x else 0) MeasureTheory.volume

Truncations of simple functions are integrable