Distribution

Results named in Tau Ceti's TauCeti.Analysis.Distribution modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.

TheoremThe constancy theorem#

On a connected open subset Ω of an oriented real vector space of dimension k + 1, a top-degree current with zero boundary, T ∘ d = 0, is a unique real multiple of the oriented integration current [[Ω]].

Orientation.existsUnique_eq_smul_integrationCurrent_of_comp_extDerivCLM_eq_zero.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E]
  [BorelSpace E] {Ω : TopologicalSpace.Opens E} {k : ℕ} (o : Orientation ℝ E (Fin (k + 1)))
  (hE : Module.finrank ℝ E = k + 1) (hΩ : IsConnected ↑Ω)
  {T : TestFunction Ω (E [⋀^Fin (k + 1)]→L[ℝ] ℝ) ⊤ →L[ℝ] ℝ}
  (hT : T ∘SL TestFunction.extDerivCLM = 0) : ∃! c, T = c • o.integrationCurrent Ω
Lean

Formalized in Tau Ceti as Orientation.existsUnique_eq_smul_integrationCurrent_of_comp_extDerivCLM_eq_zero.

Sources
LeanOrientation.existsUnique_eq_smul_integrationCurrent_of_comp_extDerivCLM_eq_zero
Uses 6 · Used by 1
Statement usesOrientation.integrationCurrent · TestFunction.extDerivCLM
Proof usesA distribution has finite order on each compact set · The derivative of a regularization · Distributions with vanishing derivatives have locally constant regularizations · Uniform first-order Taylor estimate in a parameter
Used byThe local constancy theorem

TheoremThe constancy theorem in degree zero#

On a zero-dimensional oriented real vector space every 0-current on a connected open set, which is then the whole point, is a unique real multiple of the integration current, the signed Dirac current at the origin. No boundary condition enters: the boundary of a 0-current is zero.

Orientation.existsUnique_eq_smul_integrationCurrent_of_finrank_eq_zero.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E]
  [BorelSpace E] {Ω : TopologicalSpace.Opens E} (o : Orientation ℝ E (Fin 0))
  (hE : Module.finrank ℝ E = 0) (hΩ : IsConnected ↑Ω)
  (T : TestFunction Ω (E [⋀^Fin 0]→L[ℝ] ℝ) ⊤ →L[ℝ] ℝ) : ∃! c, T = c • o.integrationCurrent Ω
Lean

Formalized in Tau Ceti as Orientation.existsUnique_eq_smul_integrationCurrent_of_finrank_eq_zero.

Sources
LeanOrientation.existsUnique_eq_smul_integrationCurrent_of_finrank_eq_zero
Uses 5
Statement usesOrientation.integrationCurrent
Proof usesA distribution has finite order on each compact set · The derivative of a regularization · Distributions with vanishing derivatives have locally constant regularizations · Uniform first-order Taylor estimate in a parameter

TheoremThe du Bois-Reymond lemma#

A function locally integrable on an open interval whose pairing with the derivative of every test function on the interval vanishes, ∫ x, deriv ψ x • f x = 0, is almost everywhere equal to a constant on the interval.

MeasureTheory.LocallyIntegrableOn.exists_ae_eq_const_Ioo_of_integral_deriv_smul_eq_zero.{u_1}
  {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {a b : ℝ} {f : ℝ → F}
  (hf : MeasureTheory.LocallyIntegrableOn f (Set.Ioo a b) MeasureTheory.volume)
  (h :
    ∀ (ψ : ℝ → ℝ), ContDiff ℝ (↑⊤) ψ → tsupport ψ ⊆ Set.Ioo a b → ∫ (x : ℝ), deriv ψ x • f x = 0) :
  ∃ c, f =ᵐ[MeasureTheory.volume.restrict (Set.Ioo a b)] fun x => c
Lean

Formalized in Tau Ceti as MeasureTheory.LocallyIntegrableOn.exists_ae_eq_const_Ioo_of_integral_deriv_smul_eq_zero.

Other forms

The du Bois-Reymond lemma for continuous functions. Formalized in Tau Ceti as ContinuousOn.exists_eqOn_const_Ioo_of_integral_deriv_smul_eq_zero.

ContinuousOn.exists_eqOn_const_Ioo_of_integral_deriv_smul_eq_zero.{u_1} {F : Type u_1}
  [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {a b : ℝ} {f : ℝ → F}
  (hf : ContinuousOn f (Set.Ioo a b))
  (h :
    ∀ (ψ : ℝ → ℝ), ContDiff ℝ (↑⊤) ψ → tsupport ψ ⊆ Set.Ioo a b → ∫ (x : ℝ), deriv ψ x • f x = 0) :
  ∃ c, Set.EqOn f (fun x => c) (Set.Ioo a b)
Sources
LeanMeasureTheory.LocallyIntegrableOn.exists_ae_eq_const_Ioo_of_integral_deriv_smul_eq_zero · ContinuousOn.exists_eqOn_const_Ioo_of_integral_deriv_smul_eq_zero
Used by 7
Used byThe Lipschitz bound for bounded harmonic functions · Weyl's lemma for continuous functions · The interior Schauder estimate on small balls · The limit in Harnack's convergence theorem is harmonic · The local Harnack inequality · Perron's theorem · The du Bois-Reymond lemma for weak derivatives

TheoremGreen's identity on Schwartz space#

for a continuous bilinear map B and an orthonormal basis b, ∫ B(f, Δg) = -∑ᵢ ∫ B(∂_{bᵢ} f, ∂_{bᵢ} g).

SchwartzMap.integral_bilinear_laplacian_right_eq_neg_sum.{u_3, u_4, u_5, u_6, u_7} {E : Type u_3}
  {F₁ : Type u_4} {F₂ : Type u_5} {F₃ : Type u_6} {ι : Type u_7} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
  {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] [NormedAddCommGroup F₁] [NormedSpace ℝ F₁]
  [NormedAddCommGroup F₂] [NormedSpace ℝ F₂] [NormedAddCommGroup F₃] [NormedSpace ℝ F₃] [Fintype ι]
  (b : OrthonormalBasis ι ℝ E) (f : SchwartzMap E F₁) (g : SchwartzMap E F₂)
  (B : F₁ →L[ℝ] F₂ →L[ℝ] F₃) :
  ∫ (x : E), (B (f x)) ((Laplacian.laplacian g) x) ∂μ =
    -∑ i, ∫ (x : E), (B ((LineDeriv.lineDerivOp (b i) f) x)) ((LineDeriv.lineDerivOp (b i) g) x) ∂μ
Lean

Formalized in Tau Ceti as SchwartzMap.integral_bilinear_laplacian_right_eq_neg_sum.

Sources
LeanSchwartzMap.integral_bilinear_laplacian_right_eq_neg_sum

TheoremThe local constancy theorem#

A top-degree current with zero boundary on an arbitrary open subset Ω of an oriented real vector space of dimension k + 1 restricts, on every connected open subset U ⊆ Ω, to a unique real multiple of the integration current [[U]].

Orientation.existsUnique_comp_monoCLM_eq_smul_integrationCurrent.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E]
  [BorelSpace E] {Ω U : TopologicalSpace.Opens E} {k : ℕ} (o : Orientation ℝ E (Fin (k + 1)))
  (hE : Module.finrank ℝ E = k + 1) {T : TestFunction Ω (E [⋀^Fin (k + 1)]→L[ℝ] ℝ) ⊤ →L[ℝ] ℝ}
  (hT : T ∘SL TestFunction.extDerivCLM = 0) (hU : U ≤ Ω) (hUc : IsConnected ↑U) :
  ∃! c, T ∘SL TestFunction.monoCLM ℝ = c • o.integrationCurrent U
Lean

Formalized in Tau Ceti as Orientation.existsUnique_comp_monoCLM_eq_smul_integrationCurrent.

Sources
LeanOrientation.existsUnique_comp_monoCLM_eq_smul_integrationCurrent
Uses 3
Statement usesOrientation.integrationCurrent · TestFunction.extDerivCLM
Proof usesThe constancy theorem

TheoremThe monotone du Bois-Reymond lemma#

A real function continuous on an open interval whose distributional derivative is nonnegative, in the sense that ∫ x, deriv ψ x * f x ≤ 0 for every nonnegative test function ψ on the interval, is monotone on the interval.

ContinuousOn.monotoneOn_of_integral_deriv_mul_nonpos {a b : ℝ} {f : ℝ → ℝ}
  (hf : ContinuousOn f (Set.Ioo a b))
  (h :
    ∀ (ψ : ℝ → ℝ),
      ContDiff ℝ (↑⊤) ψ →
        tsupport ψ ⊆ Set.Ioo a b → (∀ (x : ℝ), 0 ≤ ψ x) → ∫ (x : ℝ), deriv ψ x * f x ≤ 0) :
  MonotoneOn f (Set.Ioo a b)
Lean

Formalized in Tau Ceti as ContinuousOn.monotoneOn_of_integral_deriv_mul_nonpos.

Sources
LeanContinuousOn.monotoneOn_of_integral_deriv_mul_nonpos

TheoremPlancherel's theorem for the inverse Fourier transform of Schwartz functions# 

SchwartzMap.norm_fourierInv_toL2_eq.{u_1, u_2} {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
  [NormedAddCommGroup F] [InnerProductSpace ℂ F] [CompleteSpace F] (f : SchwartzMap E F) :
  ‖(FourierTransformInv.fourierInv f).toLp 2 MeasureTheory.volume‖ = ‖f.toLp 2 MeasureTheory.volume‖
Lean

Formalized in Tau Ceti as SchwartzMap.norm_fourierInv_toL2_eq.

Sources
LeanSchwartzMap.norm_fourierInv_toL2_eq
Used by 2
Used byThe Mihlin–Hörmander multiplier theorem on Lᵖ · The weighted Plancherel identity

TheoremThe weighted Plancherel bound#

for a Schwartz function σ, an orthonormal basis b of V indexed by ι, and N ≠ 0,

(2π) ^ (2N) ∫ ‖x‖ ^ (2N) ‖𝓕⁻ σ x‖² dx ≤ (#ι) ^ (N - 1) ∑ᵢ ‖∂_{bᵢ}^N σ‖²_{L²}.

SchwartzMap.integral_norm_pow_mul_norm_fourierInv_sq_le.{u_1, u_2, u_3} {V : Type u_1}
  {H : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V]
  [MeasurableSpace V] [BorelSpace V] [NormedAddCommGroup H] [InnerProductSpace ℂ H]
  [CompleteSpace H] {ι : Type u_3} [Fintype ι] (σ : SchwartzMap V H) (b : OrthonormalBasis ι ℝ V)
  {N : ℕ} (hN : N ≠ 0) :
  (2 * Real.pi) ^ (2 * N) * ∫ (x : V), ‖x‖ ^ (2 * N) * ‖(FourierTransformInv.fourierInv σ) x‖ ^ 2 ≤
    ↑(Fintype.card ι) ^ (N - 1) *
      ∑ i, ‖((LineDeriv.lineDerivOp (b i))^[N] σ).toLp 2 MeasureTheory.volume‖ ^ 2
Lean

Formalized in Tau Ceti as SchwartzMap.integral_norm_pow_mul_norm_fourierInv_sq_le.

Sources
LeanSchwartzMap.integral_norm_pow_mul_norm_fourierInv_sq_le
Uses 1 · Used by 1
Proof usesThe weighted Plancherel identity
Used byThe Mihlin–Hörmander multiplier theorem on Lᵖ

TheoremThe weighted Plancherel identity#

for a Schwartz function σ,

(2π) ^ (2N) ∫ ⟪x, m⟫ ^ (2N) ‖𝓕⁻ σ x‖² dx = ‖∂_m^N σ‖²_{L²}.

SchwartzMap.integral_inner_pow_mul_norm_fourierInv_sq.{u_1, u_2} {V : Type u_1} {H : Type u_2}
  [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V]
  [BorelSpace V] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
  (σ : SchwartzMap V H) (m : V) (N : ℕ) :
  (2 * Real.pi) ^ (2 * N) *
      ∫ (x : V), inner ℝ x m ^ (2 * N) * ‖(FourierTransformInv.fourierInv σ) x‖ ^ 2 =
    ‖((LineDeriv.lineDerivOp m)^[N] σ).toLp 2 MeasureTheory.volume‖ ^ 2
Lean

Formalized in Tau Ceti as SchwartzMap.integral_inner_pow_mul_norm_fourierInv_sq.

Sources
LeanSchwartzMap.integral_inner_pow_mul_norm_fourierInv_sq
Uses 1 · Used by 1
Proof usesPlancherel's theorem for the inverse Fourier transform of Schwartz functions
Used byThe weighted Plancherel bound

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.