theorem Frourio.weightedMeasure_pos_of_Ioo {σ a b : ℝ} (ha : 0 < a) (hb : a < b) : 0 < (weightedMeasure σ) (Set.Ioo a b)

weightedMeasure σ assigns positive mass to any open interval contained in (0, ∞)

theorem Frourio.continuous_ae_eq_const_on_pos {σ : ℝ} {f : ℝ → ℂ} {c : ℂ} (hf : Continuous f) (h_ae : (fun (x : ℝ) => f x) =ᵐ[weightedMeasure σ] fun (x : ℝ) => c) (x : ℝ) : x > 0 → f x = c

If a continuous function agrees almost everywhere with a constant, it is constant on (0, ∞).

theorem Frourio.continuous_ae_eq_on_pos {σ : ℝ} {f g : ℝ → ℂ} (hf : Continuous f) (hg : Continuous g) (h_ae : f =ᵐ[weightedMeasure σ] g) (x : ℝ) : x > 0 → f x = g x

If two continuous functions agree almost everywhere for the weighted measure, they coincide on (0, ∞).

theorem Frourio.coe_cast_eq {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} [NormedAddCommGroup E] {μ ν : MeasureTheory.Measure α} (h : μ = ν) (f : ↥(MeasureTheory.Lp E p μ)) : ↑↑(cast ⋯ f) =ᵐ[μ] ↑↑f

Coercion of cast between Lp spaces with equal measures

theorem Frourio.Hσ_cast_preserves_ae {σ : ℝ} (f : ℝ → ℂ) (h_L2 : MeasureTheory.MemLp f 2 (weightedMeasure σ)) (h_eq : weightedMeasure σ = mulHaar.withDensity fun (x : ℝ) => ENNReal.ofReal (x ^ (2 * σ - 1))) : let g_lp := MeasureTheory.MemLp.toLp f h_L2; let g := cast ⋯ g_lp; Hσ.toFun g =ᵐ[weightedMeasure σ] ↑↑(MeasureTheory.MemLp.toLp f h_L2)

theorem Frourio.cast_preserves_ae_eq {σ : ℝ} (h_eq : weightedMeasure σ = mulHaar.withDensity fun (x : ℝ) => ENNReal.ofReal (x ^ (2 * σ - 1))) (f : ℝ → ℂ) (h_L2 : MeasureTheory.MemLp f 2 (weightedMeasure σ)) : let g_lp := MeasureTheory.MemLp.toLp f h_L2; let g := cast ⋯ g_lp; Hσ.toFun g =ᵐ[weightedMeasure σ] f

Cast preserves a.e. equality for Lp functions

noncomputable def Frourio.create_mollifier (δ : ℝ) : ℝ → ℝ

Helper function: Create mollifier with support on [-δ, δ]

Equations

• Frourio.create_mollifier δ = fun (x : ℝ) => if |x| < δ then Real.exp (-1 / (δ ^ 2 - x ^ 2)) / ∫ (t : ℝ) in Set.Ioo (-δ) δ, Real.exp (-1 / (δ ^ 2 - t ^ 2)) else 0

theorem Frourio.one_le_two_pow (k : ℕ) : 1 ≤ 2 ^ k

Powers of 2 are at least 1

theorem Frourio.schwartz_map_decay_from_bounds (f : ℝ → ℂ) (hf_decay : ∀ (k n : ℕ), ∃ C > 0, ∀ (x : ℝ), (1 + ‖x‖) ^ k * ‖iteratedDeriv n f x‖ ≤ C) (p : ℕ × ℕ) : ∃ C > 0, ∀ (x : ℝ), (1 + ‖x‖) ^ p.1 * ‖iteratedDeriv p.2 f x‖ ≤ C

The decay property required for SchwartzMap construction

theorem Frourio.contDiff_convolution_mollifier {φ : ℝ → ℂ} {η : ℝ → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hη_smooth : ContDiff ℝ (↑⊤) η) (hη_supp : HasCompactSupport η) : ContDiff ℝ ↑⊤ fun (x : ℝ) => ∫ (y : ℝ), ↑(η y) * φ (x - y)

Convolution with a smooth compactly supported mollifier preserves smoothness

def Frourio.SchwartzRestricted : Set (ℝ → ℂ)

Schwartz functions restricted to (0,∞)

Equations

• Frourio.SchwartzRestricted = {f : ℝ → ℂ | ∃ (g : SchwartzMap ℝ ℂ), ∀ x > 0, f x = g x}

structure Frourio.UnboundedOperatorDomain (σ : ℝ) : Type

Domain of unbounded operators on Hσ

• carrier : Set ↥(Hσ σ)
• dense : DenseRange fun (x : ↑self.carrier) => ↑x
• measurable (f : ↥(Hσ σ)) : f ∈ self.carrier → Measurable ↑↑f