Function

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

TheoremCampanato's theorem#

Let α > 0, and let f be locally integrable, with mean oscillation on every closed ball of radius r > 0 at most M r^α. Then the precise representative of f is α-Hölder continuous, with constant 2 · 2^α · 2ⁿ / (1 - 2^(-α)) · M, where n is the dimension. It agrees with f almost everywhere (TauCeti.MeasureTheory.ae_eq_preciseRepresentative).

TauCeti.MeasureTheory.holderWith_preciseRepresentative_of_setAverage_norm_sub_le.{u_1, u_2}
  {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure]
  [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {f : E → F} {α M : NNReal} (hα : 0 < α)
  (hf : MeasureTheory.LocallyIntegrable f μ)
  (hosc :
    ∀ (x : E) (r : ℝ),
      0 < r →
        ⨍ (y : E) in Metric.closedBall x r, ‖f y - ⨍ (z : E) in Metric.closedBall x r, f z ∂μ‖ ∂μ ≤
          ↑M * r ^ ↑α) :
  HolderWith ((2 * 2 ^ ↑α * (2 ^ Module.finrank ℝ E / (1 - 2 ^ (-↑α)))).toNNReal * M) α
    (TauCeti.MeasureTheory.preciseRepresentative μ f)
Lean

Formalized in Tau Ceti as TauCeti.MeasureTheory.holderWith_preciseRepresentative_of_setAverage_norm_sub_le.

Sources
LeanTauCeti.MeasureTheory.holderWith_preciseRepresentative_of_setAverage_norm_sub_le
Uses 1
Proof usesThe local Campanato estimate

TheoremDiscrete Hölder estimate for a disjoint family of intervals (sᵢ, tᵢ] in [0, T]#

the p-th power of the sum of the distances between the piecewise constant interpolant at times sᵢ and tᵢ is at most (|⋃ (sᵢ, tᵢ]| + k τ) ^ (p - 1) times the discrete p-action up to time T, where k is the number of intervals. As τ → 0 the factor tends to the one in the Hölder estimate AbsolutelyContinuousOnInterval.edist_rpow_le_mul_curveAction for curves.

TauCeti.sum_edist_ceil_div_rpow_le.{u_1} {X : Type u_1} [TopologicalSpace X]
  [WeakPseudoEMetricSpace X] {p : ℝ} {τ : NNReal} {U : ℕ → X} (hp : 1 ≤ p) (hτ : 0 < τ) {T : ℝ}
  (hT : 0 ≤ T) {E : ℕ × (ℕ → ℝ × ℝ)} (hE : E ∈ AbsolutelyContinuousOnInterval.disjWithin 0 T) :
  (∑ i ∈ Finset.range E.1, edist (U ⌈(E.2 i).1 / ↑τ⌉₊) (U ⌈(E.2 i).2 / ↑τ⌉₊)) ^ p ≤
    (MeasureTheory.volume (⋃ i ∈ Finset.range E.1, Set.uIoc (E.2 i).1 (E.2 i).2) + ↑E.1 * ↑τ) ^
        (p - 1) *
      ∑ n ∈ Finset.range ⌈T / ↑τ⌉₊, edist (U n) (U (n + 1)) ^ p / ↑τ ^ (p - 1)
Lean

Formalized in Tau Ceti as TauCeti.sum_edist_ceil_div_rpow_le.

Sources
LeanTauCeti.sum_edist_ceil_div_rpow_le

TheoremDunford–Pettis theorem#

For a finite measure, a subset of scalar L¹ has weakly compact closure exactly when it is norm bounded and uniformly integrable.

MeasureTheory.Lp.isCompact_closure_toWeakSpace_iff_isBounded_and_unifIntegrable.{u_1, u_2}
  {α : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [MeasureTheory.IsFiniteMeasure μ] {A : Set ↥(MeasureTheory.Lp 𝕜 1 μ)} :
  IsCompact (closure (⇑(toWeakSpace 𝕜 ↥(MeasureTheory.Lp 𝕜 1 μ)) '' A)) ↔
    Bornology.IsBounded A ∧ MeasureTheory.UnifIntegrable (fun f => ↑↑↑f) 1 μ
Lean

Formalized in Tau Ceti as MeasureTheory.Lp.isCompact_closure_toWeakSpace_iff_isBounded_and_unifIntegrable.

Other forms

Dunford–Pettis theorem, classical form. Formalized in Tau Ceti as MeasureTheory.Lp.isCompact_closure_toWeakSpace_iff_isBounded_and_forall_setIntegral_le.

MeasureTheory.Lp.isCompact_closure_toWeakSpace_iff_isBounded_and_forall_setIntegral_le.{u_1, u_2}
  {α : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [MeasureTheory.IsFiniteMeasure μ] {A : Set ↥(MeasureTheory.Lp 𝕜 1 μ)} :
  IsCompact (closure (⇑(toWeakSpace 𝕜 ↥(MeasureTheory.Lp 𝕜 1 μ)) '' A)) ↔
    Bornology.IsBounded A ∧
      ∀ ε > 0,
        ∃ δ > 0,
          ∀ f ∈ A,
            ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → ∫ (x : α) in s, ‖↑↑f x‖ ∂μ ≤ ε

Dunford–Pettis theorem. Formalized in Tau Ceti as MeasureTheory.Lp.isCompact_closure_toWeakSpace_iff_uniformIntegrable.

MeasureTheory.Lp.isCompact_closure_toWeakSpace_iff_uniformIntegrable.{u_1, u_2} {α : Type u_1}
  {𝕜 : Type u_2} [RCLike 𝕜] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [MeasureTheory.IsFiniteMeasure μ] {A : Set ↥(MeasureTheory.Lp 𝕜 1 μ)} :
  IsCompact (closure (⇑(toWeakSpace 𝕜 ↥(MeasureTheory.Lp 𝕜 1 μ)) '' A)) ↔
    MeasureTheory.UniformIntegrable (fun f => ↑↑↑f) 1 μ

Dunford–Pettis theorem, sufficiency. Formalized in Tau Ceti as MeasureTheory.Lp.isCompact_closure_toWeakSpace_of_uniformIntegrable.

MeasureTheory.Lp.isCompact_closure_toWeakSpace_of_uniformIntegrable.{u_1, u_2} {α : Type u_1}
  {𝕜 : Type u_2} [RCLike 𝕜] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [MeasureTheory.IsFiniteMeasure μ] {A : Set ↥(MeasureTheory.Lp 𝕜 1 μ)}
  (hA : MeasureTheory.UniformIntegrable (fun f => ↑↑↑f) 1 μ) :
  IsCompact (closure (⇑(toWeakSpace 𝕜 ↥(MeasureTheory.Lp 𝕜 1 μ)) '' A))

Dunford–Pettis theorem, necessity. Formalized in Tau Ceti as MeasureTheory.Lp.uniformIntegrable_of_isCompact_closure_toWeakSpace.

MeasureTheory.Lp.uniformIntegrable_of_isCompact_closure_toWeakSpace.{u_1, u_2} {α : Type u_1}
  {𝕜 : Type u_2} [RCLike 𝕜] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [MeasureTheory.IsFiniteMeasure μ] {A : Set ↥(MeasureTheory.Lp 𝕜 1 μ)}
  (hA : IsCompact (closure (⇑(toWeakSpace 𝕜 ↥(MeasureTheory.Lp 𝕜 1 μ)) '' A))) :
  MeasureTheory.UniformIntegrable (fun f => ↑↑↑f) 1 μ
Sources
LeanMeasureTheory.Lp.isCompact_closure_toWeakSpace_iff_isBounded_and_unifIntegrable · MeasureTheory.Lp.isCompact_closure_toWeakSpace_iff_isBounded_and_forall_setIntegral_le · MeasureTheory.Lp.isCompact_closure_toWeakSpace_iff_uniformIntegrable · MeasureTheory.Lp.isCompact_closure_toWeakSpace_of_uniformIntegrable · MeasureTheory.Lp.uniformIntegrable_of_isCompact_closure_toWeakSpace
Uses 3
Proof usesGrothendieck's lemma · Milman–Pettis theorem · Šmulian's theorem

TheoremEilenberg's inequality, integral form#

for f K-Lipschitz on A with values in an m-dimensional real normed space with additive Haar measure μ, and t real, ∫⁻ y, μH[t] (A ∩ f ⁻¹' {y}) ∂μ ≤ μ (ball 0 1) * K ^ m * μH[m + t] A.

The fiber-measure function y ↦ μH[t] (A ∩ f ⁻¹' {y}) need not be measurable, and for a non-measurable integrand ∫⁻ is the lower Lebesgue integral (the supremum of the integrals of the measurable functions below it). So this bounds the lower integral of the fiber measures. The upper-integral form is LipschitzOnWith.exists_measurable_hausdorffMeasure_inter_preimage_le: a measurable G dominating the fiber measures with ∫⁻ y, G y ∂μ ≤ μ (ball 0 1) * K ^ m * μH[m + t] A.

LipschitzOnWith.lintegral_hausdorffMeasure_inter_preimage_le.{u_1, u_2} {X : Type u_1}
  {Y : Type u_2} [EMetricSpace X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] [FiniteDimensional ℝ Y]
  [MeasurableSpace Y] [BorelSpace Y] (μ : MeasureTheory.Measure Y) [μ.IsAddHaarMeasure] {K : NNReal}
  {f : X → Y} {A : Set X} {t : ℝ} [MeasurableSpace X] [BorelSpace X] (hf : LipschitzOnWith K f A) :
  ∫⁻ (y : Y), (MeasureTheory.Measure.hausdorffMeasure t) (A ∩ f ⁻¹' {y}) ∂μ ≤
    μ (Metric.ball 0 1) * ↑K ^ Module.finrank ℝ Y *
      (MeasureTheory.Measure.hausdorffMeasure (↑(Module.finrank ℝ Y) + t)) A
Lean

Formalized in Tau Ceti as LipschitzOnWith.lintegral_hausdorffMeasure_inter_preimage_le.

Other forms

Eilenberg's inequality, in its strong form. Formalized in Tau Ceti as LipschitzOnWith.exists_measurable_hausdorffMeasure_inter_preimage_le.

LipschitzOnWith.exists_measurable_hausdorffMeasure_inter_preimage_le.{u_1, u_2} {X : Type u_1}
  {Y : Type u_2} [EMetricSpace X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] [FiniteDimensional ℝ Y]
  [MeasurableSpace Y] [BorelSpace Y] (μ : MeasureTheory.Measure Y) [μ.IsAddHaarMeasure] {K : NNReal}
  {f : X → Y} {A : Set X} {t : ℝ} [MeasurableSpace X] [BorelSpace X] (hf : LipschitzOnWith K f A) :
  ∃ G,
    Measurable G ∧
      (∀ (y : Y), (MeasureTheory.Measure.hausdorffMeasure t) (A ∩ f ⁻¹' {y}) ≤ G y) ∧
        ∫⁻ (y : Y), G y ∂μ ≤
          μ (Metric.ball 0 1) * ↑K ^ Module.finrank ℝ Y *
            (MeasureTheory.Measure.hausdorffMeasure (↑(Module.finrank ℝ Y) + t)) A
Sources
LeanLipschitzOnWith.lintegral_hausdorffMeasure_inter_preimage_le · LipschitzOnWith.exists_measurable_hausdorffMeasure_inter_preimage_le

TheoremFatou's lemma for the Lᵖ seminorm of ℝ≥0∞-valued functions#

Fatou's lemma for the Lᵖ seminorm of ℝ≥0∞-valued functions, at every exponent p : ℝ≥0∞ (including 0 and ∞) and along any countably generated NeBot filter. Almost everywhere measurability of the limit is deduced from the pointwise convergence.

TauCeti.eLpNorm_ennreal_le_of_ae_tendsto.{u_1, u_2} {α : Type u_1} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α} {p : ENNReal} {ι : Type u_2} {u : Filter ι} [u.NeBot]
  [u.IsCountablyGenerated] {f : ι → α → ENNReal} {g : α → ENNReal} {C : ENNReal}
  (hf : ∀ (i : ι), AEMeasurable (f i) μ)
  (hlim : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun i => f i x) u (nhds (g x)))
  (hle : ∀ᶠ (i : ι) in u, MeasureTheory.eLpNorm (f i) p μ ≤ C) : MeasureTheory.eLpNorm g p μ ≤ C
Lean

Formalized in Tau Ceti as TauCeti.eLpNorm_ennreal_le_of_ae_tendsto.

Other forms

Fatou's lemma for the Lᵖ seminorm of ℝ≥0∞-valued functions. Formalized in Tau Ceti as TauCeti.eLpNorm_le_of_ae_tendsto_ennreal.

TauCeti.eLpNorm_le_of_ae_tendsto_ennreal.{u_1} {α : Type u_1} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α} {p : ENNReal} (hp0 : p ≠ 0) (hp : p ≠ ⊤) {f : ℕ → α → ENNReal}
  {g : α → ENNReal} {c : ENNReal} (hf : ∀ (n : ℕ), AEMeasurable (f n) μ)
  (hlim : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) Filter.atTop (nhds (g x)))
  (hle : ∀ (n : ℕ), MeasureTheory.eLpNorm (f n) p μ ≤ c) : MeasureTheory.eLpNorm g p μ ≤ c
Sources
LeanTauCeti.eLpNorm_ennreal_le_of_ae_tendsto · TauCeti.eLpNorm_le_of_ae_tendsto_ennreal

TheoremThe Fréchet--Kolmogorov compactness criterion#

For 1 ≤ p < ∞, a family S of Lᵖ functions is totally bounded as soon as it is bounded in Lᵖ, its translation increments are uniformly small in Lᵖ, and it is uniformly tight in the sense of MeasureTheory.UnifTight.

Dropping either of the last two hypotheses breaks the conclusion: on ℝ the concentrating family n ^ (1/p) 1_{[0, 1/n]} satisfies all but the smallness of translations, and the escaping family f(· - n) of translates of a single nonzero f satisfies all but tightness, and neither is totally bounded.

TauCeti.totallyBounded_of_comp_add_sub_of_unifTight.{u_1, u_2} {E : Type u_1} {F : Type u_2}
  [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] [ProperSpace E] [NormedAddCommGroup F]
  [NormedSpace ℝ F] [FiniteDimensional ℝ F] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure]
  {p : ENNReal} [Fact (1 ≤ p)] (hp' : p ≠ ⊤) {S : Set ↥(MeasureTheory.Lp F p mu)} {M : ENNReal}
  (hM : M ≠ ⊤) (hbdd : ∀ f ∈ S, MeasureTheory.eLpNorm (↑↑f) p mu ≤ M)
  (htrans :
    ∀ (ε : ENNReal),
      0 < ε →
        ∃ δ > 0,
          ∀ f ∈ S,
            ∀ (h : E), ‖h‖ < δ → MeasureTheory.eLpNorm (fun x => ↑↑f (x + h) - ↑↑f x) p mu ≤ ε)
  (htight : MeasureTheory.UnifTight (fun i => ↑↑↑i) p mu) : TotallyBounded S
Lean

Formalized in Tau Ceti as TauCeti.totallyBounded_of_comp_add_sub_of_unifTight.

Sources
LeanTauCeti.totallyBounded_of_comp_add_sub_of_unifTight
Uses 2 · Used by 1
Proof usesThe Arzelà–Ascoli theorem in C(X, Y) · Hölder's bound on an average
Used byThe Fréchet--Kolmogorov criterion for a family vanishing almost everywhere off a fixed bounded set

TheoremThe Fréchet--Kolmogorov criterion for a family vanishing almost everywhere off a fixed bounded set#

The Fréchet--Kolmogorov criterion for a family vanishing almost everywhere off a fixed bounded set, the form that Rellich--Kondrachov for W^{1,p}_0(Ω) consumes. For such functions the tightness hypothesis is automatic, so an Lᵖ-bounded family whose translation increments are uniformly small in Lᵖ is totally bounded.

TauCeti.totallyBounded_of_comp_add_sub_of_isBounded_of_ae_eq_zero_compl.{u_1, u_2} {E : Type u_1}
  {F : Type u_2} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] [ProperSpace E]
  [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {mu : MeasureTheory.Measure E}
  [mu.IsAddHaarMeasure] {p : ENNReal} [Fact (1 ≤ p)] (hp' : p ≠ ⊤)
  {S : Set ↥(MeasureTheory.Lp F p mu)} {s : Set E} (hs : Bornology.IsBounded s)
  (hsupp : ∀ f ∈ S, ∀ᵐ (x : E) ∂mu, x ∉ s → ↑↑f x = 0) {M : ENNReal} (hM : M ≠ ⊤)
  (hbdd : ∀ f ∈ S, MeasureTheory.eLpNorm (↑↑f) p mu ≤ M)
  (htrans :
    ∀ (ε : ENNReal),
      0 < ε →
        ∃ δ > 0,
          ∀ f ∈ S,
            ∀ (h : E), ‖h‖ < δ → MeasureTheory.eLpNorm (fun x => ↑↑f (x + h) - ↑↑f x) p mu ≤ ε) :
  TotallyBounded S
Lean

Formalized in Tau Ceti as TauCeti.totallyBounded_of_comp_add_sub_of_isBounded_of_ae_eq_zero_compl.

Sources
LeanTauCeti.totallyBounded_of_comp_add_sub_of_isBounded_of_ae_eq_zero_compl
Uses 1 · Used by 1
Proof usesThe Fréchet--Kolmogorov compactness criterion
Used byRellich–Kondrachov on bounded Lipschitz domains

TheoremFundamental theorem for absolutely continuous curves, integrability#

the metric derivative of an absolutely continuous curve on [a, b] has finite integral over [a, b].

AbsolutelyContinuousOnInterval.lintegral_metricDerivative_lt_top.{u_1} {X : Type u_1}
  [PseudoMetricSpace X] {γ : ℝ → X} {a b : ℝ} (hγ : AbsolutelyContinuousOnInterval γ a b) :
  ∫⁻ (r : ℝ) in Set.uIoc a b, TauCeti.metricDerivative γ r < ⊤
Lean

Formalized in Tau Ceti as AbsolutelyContinuousOnInterval.lintegral_metricDerivative_lt_top.

Other forms

Fundamental theorem for absolutely continuous curves, existence of the metric derivative. Formalized in Tau Ceti as AbsolutelyContinuousOnInterval.ae_tendsto_metricDerivative.

AbsolutelyContinuousOnInterval.ae_tendsto_metricDerivative.{u_1} {X : Type u_1}
  [PseudoMetricSpace X] {γ : ℝ → X} {a b : ℝ} (hγ : AbsolutelyContinuousOnInterval γ a b) :
  ∀ᵐ (t : ℝ),
    t ∈ Set.uIcc a b →
      Filter.Tendsto (fun s => edist (γ s) (γ t) / edist s t) (nhdsWithin t {t}ᶜ)
        (nhds (TauCeti.metricDerivative γ t))

Fundamental theorem for absolutely continuous curves, the distance bound. Formalized in Tau Ceti as AbsolutelyContinuousOnInterval.edist_le_lintegral_metricDerivative.

AbsolutelyContinuousOnInterval.edist_le_lintegral_metricDerivative.{u_1} {X : Type u_1}
  [PseudoMetricSpace X] {γ : ℝ → X} {a b : ℝ} (hγ : AbsolutelyContinuousOnInterval γ a b) {s u : ℝ}
  (hs : s ∈ Set.uIcc a b) (hu : u ∈ Set.uIcc a b) :
  edist (γ s) (γ u) ≤ ∫⁻ (r : ℝ) in Set.uIoc s u, TauCeti.metricDerivative γ r
Sources
LeanAbsolutelyContinuousOnInterval.lintegral_metricDerivative_lt_top · AbsolutelyContinuousOnInterval.ae_tendsto_metricDerivative · AbsolutelyContinuousOnInterval.edist_le_lintegral_metricDerivative
Used by 4
Used byJordan index theorem (orientation sign dichotomy) · TauCeti.Green.green_ac_winding · Hölder estimate along a curve · Lisini's superposition principle in a complete separable metric space

TheoremHölder estimate along a curve#

if γ is absolutely continuous on [a, b] and 1 ≤ p, then edist (γ s) (γ u) ^ p ≤ edist s u ^ (p - 1) * curveAction p γ s u for all s, u ∈ [a, b]. In particular a curve of finite p-action with 1 < p is (1 - 1 / p)-Hölder continuous.

AbsolutelyContinuousOnInterval.edist_rpow_le_mul_curveAction.{u_1} {X : Type u_1}
  [PseudoMetricSpace X] {p : ℝ} {γ : ℝ → X} {a b : ℝ} (hγ : AbsolutelyContinuousOnInterval γ a b)
  (hp : 1 ≤ p) {s u : ℝ} (hs : s ∈ Set.uIcc a b) (hu : u ∈ Set.uIcc a b) :
  edist (γ s) (γ u) ^ p ≤ edist s u ^ (p - 1) * TauCeti.curveAction p γ s u
Lean

Formalized in Tau Ceti as AbsolutelyContinuousOnInterval.edist_rpow_le_mul_curveAction.

Sources
LeanAbsolutelyContinuousOnInterval.edist_rpow_le_mul_curveAction
Uses 2 · Used by 3
Proof usesFundamental theorem for absolutely continuous curves, integrability · Hölder's inequality for the integral of a product
Used byHölder–Markov estimate · Lisini's superposition principle in a complete separable metric space · Uniqueness of Wasserstein geodesics

TheoremHölder's inequality for the integral of a product#

‖∫ u v‖ ≤ ‖u‖_p ‖v‖_q for Hölder conjugate exponents p and q.

TauCeti.enorm_integral_mul_le.{u_1, u_4} {α : Type u_1} {mα : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {𝕜 : Type u_4} [NonUnitalNormedRing 𝕜] [NormedSpace ℝ 𝕜]
  {p q : ENNReal} [p.HolderConjugate q] {u v : α → 𝕜} :
  ‖∫ (x : α), u x * v x ∂μ‖ₑ ≤ MeasureTheory.eLpNorm u p μ * MeasureTheory.eLpNorm v q μ
Lean

Formalized in Tau Ceti as TauCeti.enorm_integral_mul_le.

Other forms

Hölder's inequality for the integral of an inner product. Formalized in Tau Ceti as TauCeti.enorm_integral_inner_le.

TauCeti.enorm_integral_inner_le.{u_1, u_4, u_5} {α : Type u_1} {mα : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {𝕜 : Type u_4} {H : Type u_5} [RCLike 𝕜] [NormedAddCommGroup H]
  [InnerProductSpace 𝕜 H] {p q : ENNReal} [p.HolderConjugate q] {u v : α → H} :
  ‖∫ (x : α), inner 𝕜 (u x) (v x) ∂μ‖ₑ ≤ MeasureTheory.eLpNorm u p μ * MeasureTheory.eLpNorm v q μ

Hölder's inequality in extended-valued ∫⁻ form, raised to the power r. Formalized in Tau Ceti as TauCeti.rpow_lintegral_le_measure_univ_rpow_mul.

TauCeti.rpow_lintegral_le_measure_univ_rpow_mul.{u_1} {α : Type u_1} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α} {u : α → ENNReal} (hu : AEMeasurable u μ) {r : ℝ} (hr : 1 ≤ r) :
  (∫⁻ (x : α), u x ∂μ) ^ r ≤ μ Set.univ ^ (r - 1) * ∫⁻ (x : α), u x ^ r ∂μ
Sources
LeanTauCeti.enorm_integral_mul_le · TauCeti.enorm_integral_inner_le · TauCeti.rpow_lintegral_le_measure_univ_rpow_mul
Used by 12
Used byThe Mihlin–Hörmander multiplier theorem on Lᵖ · The interior Calderón–Zygmund estimate for continuous coefficients · The interior Schauder estimate on small balls · Rellich–Kondrachov on bounded Lipschitz domains · The one-dimensional Poincaré inequality · Hölder estimate along a curve · Cauchy–Schwarz on a circle · Hölder's bound on an average · The Calderón–Zygmund theorem · The Riesz–Thorin interpolation theorem · Lisini's superposition principle in a complete separable metric space · The Efron–Stein inequality on Measure.pi over a finite index type

TheoremJensen's inequality for the conditional expectation, as an inequality of lintegrals#

for 1 ≤ p, the p-th power of the norm of μ[f | m] integrates to at most that of f. Unlike Mathlib's integral_norm_condExp_rpow_le, this needs no integrability of ‖f‖ ^ p.

TauCeti.MeasureTheory.lintegral_enorm_condExp_rpow_le.{u_1, u_2} {Ω : Type u_1} {E : Type u_2}
  [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {m m₀ : MeasurableSpace Ω}
  {μ : MeasureTheory.Measure Ω} {f : Ω → E} (hf : MeasureTheory.AEStronglyMeasurable f μ) {p : ℝ}
  (hp : 1 ≤ p) : ∫⁻ (ω : Ω), ‖μ[f | m] ω‖ₑ ^ p ∂μ ≤ ∫⁻ (ω : Ω), ‖f ω‖ₑ ^ p ∂μ
Lean

Formalized in Tau Ceti as TauCeti.MeasureTheory.lintegral_enorm_condExp_rpow_le.

Sources
LeanTauCeti.MeasureTheory.lintegral_enorm_condExp_rpow_le
Used by 1
Used byThe Benamou–Brenier upper bound

TheoremThe local Campanato estimate#

Let α > 0 and d = dist x y. If f has mean oscillation at most M r^α on closedBall x r for 0 < r ≤ 2 d and on closedBall y r for 0 < r ≤ d, and is integrable on closedBall x (2 d), then the precise representatives of f at x and y differ by at most 2 · 2^α · 2ⁿ / (1 - 2^(-α)) · M d^α, where n is the dimension.

TauCeti.MeasureTheory.dist_preciseRepresentative_le_of_setAverage_norm_sub_le.{u_1, u_2}
  {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure]
  [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {f : E → F} {x : E} {M α : ℝ} {y : E}
  (hα : 0 < α) (hf : MeasureTheory.IntegrableOn f (Metric.closedBall x (2 * dist x y)) μ)
  (hoscx :
    ∀ (r : ℝ),
      0 < r →
        r ≤ 2 * dist x y →
          ⨍ (z : E) in Metric.closedBall x r,
              ‖f z - ⨍ (w : E) in Metric.closedBall x r, f w ∂μ‖ ∂μ ≤
            M * r ^ α)
  (hoscy :
    ∀ (r : ℝ),
      0 < r →
        r ≤ dist x y →
          ⨍ (z : E) in Metric.closedBall y r,
              ‖f z - ⨍ (w : E) in Metric.closedBall y r, f w ∂μ‖ ∂μ ≤
            M * r ^ α) :
  dist (TauCeti.MeasureTheory.preciseRepresentative μ f x)
      (TauCeti.MeasureTheory.preciseRepresentative μ f y) ≤
    2 * 2 ^ α * (2 ^ Module.finrank ℝ E / (1 - 2 ^ (-α))) * (M * dist x y ^ α)
Lean

Formalized in Tau Ceti as TauCeti.MeasureTheory.dist_preciseRepresentative_le_of_setAverage_norm_sub_le.

Sources
LeanTauCeti.MeasureTheory.dist_preciseRepresentative_le_of_setAverage_norm_sub_le
Used by 3
Used byThe interior Schauder estimate on small balls · The pointwise Morrey estimate · Campanato's theorem

TheoremLusin's theorem#

A measurable map f from a weakly regular measure space into a second-countable topological space is continuous on a closed set F ⊆ s with μ (s \ F) < ε, for every measurable set s of finite measure and every ε > 0.

Measurable.exists_isClosed_measure_sdiff_lt_continuousOn.{u_1, u_2} {X : Type u_1} {Y : Type u_2}
  [TopologicalSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] [TopologicalSpace Y]
  [SecondCountableTopology Y] [MeasurableSpace Y] [OpensMeasurableSpace Y]
  {μ : MeasureTheory.Measure X} [μ.WeaklyRegular] {f : X → Y} {s : Set X} {ε : ENNReal}
  (hf : Measurable f) (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (hε : ε ≠ 0) :
  ∃ F ⊆ s, IsClosed F ∧ μ (s \ F) < ε ∧ ContinuousOn f F
Lean

Formalized in Tau Ceti as Measurable.exists_isClosed_measure_sdiff_lt_continuousOn.

Other forms

Lusin's theorem for an almost-everywhere measurable map. Formalized in Tau Ceti as AEMeasurable.exists_isClosed_measure_sdiff_lt_continuousOn.

AEMeasurable.exists_isClosed_measure_sdiff_lt_continuousOn.{u_1, u_2} {X : Type u_1} {Y : Type u_2}
  [TopologicalSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] [TopologicalSpace Y]
  [SecondCountableTopology Y] [MeasurableSpace Y] [OpensMeasurableSpace Y]
  {μ : MeasureTheory.Measure X} [μ.WeaklyRegular] {f : X → Y} {s : Set X} {ε : ENNReal}
  (hf : AEMeasurable f μ) (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (hε : ε ≠ 0) :
  ∃ F ⊆ s, IsClosed F ∧ μ (s \ F) < ε ∧ ContinuousOn f F

Lusin's theorem. Formalized in Tau Ceti as MeasureTheory.AEStronglyMeasurable.exists_isClosed_measure_sdiff_lt_continuousOn.

MeasureTheory.AEStronglyMeasurable.exists_isClosed_measure_sdiff_lt_continuousOn.{u_1, u_3}
  {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] [OpensMeasurableSpace X]
  {μ : MeasureTheory.Measure X} [μ.WeaklyRegular] {s : Set X} {ε : ENNReal} {Z : Type u_3}
  [TopologicalSpace Z] [TopologicalSpace.PseudoMetrizableSpace Z] {g : X → Z}
  (hg : MeasureTheory.AEStronglyMeasurable g μ) (hs : MeasurableSet s) (hμs : μ s ≠ ⊤)
  (hε : ε ≠ 0) : ∃ F ⊆ s, IsClosed F ∧ μ (s \ F) < ε ∧ ContinuousOn g F

Lusin's theorem for a strongly measurable map into a pseudometrizable space. Formalized in Tau Ceti as MeasureTheory.StronglyMeasurable.exists_isClosed_measure_sdiff_lt_continuousOn.

MeasureTheory.StronglyMeasurable.exists_isClosed_measure_sdiff_lt_continuousOn.{u_1, u_3}
  {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] [OpensMeasurableSpace X]
  {μ : MeasureTheory.Measure X} [μ.WeaklyRegular] {s : Set X} {ε : ENNReal} {Z : Type u_3}
  [TopologicalSpace Z] [TopologicalSpace.PseudoMetrizableSpace Z] {g : X → Z}
  (hg : MeasureTheory.StronglyMeasurable g) (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (hε : ε ≠ 0) :
  ∃ F ⊆ s, IsClosed F ∧ μ (s \ F) < ε ∧ ContinuousOn g F
Sources
LeanMeasurable.exists_isClosed_measure_sdiff_lt_continuousOn · AEMeasurable.exists_isClosed_measure_sdiff_lt_continuousOn · MeasureTheory.AEStronglyMeasurable.exists_isClosed_measure_sdiff_lt_continuousOn · MeasureTheory.StronglyMeasurable.exists_isClosed_measure_sdiff_lt_continuousOn

TheoremPettis' theorem in a separable inner product space#

A function into a separable inner product space is almost everywhere strongly measurable exactly when it is weakly measurable, that is, when each of its coordinates t ↦ ⟪v, h t⟫ is almost everywhere strongly measurable.

TauCeti.aestronglyMeasurable_iff_forall_inner.{u_1, u_2, u_3} {α : Type u_1} {𝕜 : Type u_2}
  {E : Type u_3} {x✝ : MeasurableSpace α} {μ : MeasureTheory.Measure α} [RCLike 𝕜]
  [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [TopologicalSpace.SeparableSpace E] {h : α → E} :
  MeasureTheory.AEStronglyMeasurable h μ ↔
    ∀ (v : E), MeasureTheory.AEStronglyMeasurable (fun t => inner 𝕜 v (h t)) μ
Lean

Formalized in Tau Ceti as TauCeti.aestronglyMeasurable_iff_forall_inner.

Other forms

Pettis' theorem for the dual of a separable Hilbert space. Formalized in Tau Ceti as TauCeti.aestronglyMeasurable_strongDual_iff_forall_apply.

TauCeti.aestronglyMeasurable_strongDual_iff_forall_apply.{u_1, u_2, u_3} {α : Type u_1}
  {𝕜 : Type u_2} {E : Type u_3} {x✝ : MeasurableSpace α} {μ : MeasureTheory.Measure α} [RCLike 𝕜]
  [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [TopologicalSpace.SeparableSpace E]
  [CompleteSpace E] {g : α → StrongDual 𝕜 E} :
  MeasureTheory.AEStronglyMeasurable g μ ↔
    ∀ (v : E), MeasureTheory.AEStronglyMeasurable (fun t => (g t) v) μ
Sources
LeanTauCeti.aestronglyMeasurable_iff_forall_inner · TauCeti.aestronglyMeasurable_strongDual_iff_forall_apply
Used by 1
Used byExistence of weak solutions for linear parabolic equations

TheoremSard's lemma for Lipschitz maps#

The image of the set where the dim U-dimensional Jacobian of a Lipschitz map f : U → V vanishes is null for the dim U-dimensional Euclidean Hausdorff measure.

LipschitzWith.euclideanHausdorffMeasure_image_setOf_normDet_fderiv_eq_zero.{u_1, u_2} {U : Type u_1}
  {V : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [FiniteDimensional ℝ U]
  [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace U]
  [BorelSpace U] [MeasurableSpace V] [BorelSpace V] {f : U → V} {K : NNReal}
  (hf : LipschitzWith K f) :
  (MeasureTheory.Measure.euclideanHausdorffMeasure (Module.finrank ℝ U))
      (f '' {x | (↑(fderiv ℝ f x)).normDet = 0}) =
    0
Lean

Formalized in Tau Ceti as LipschitzWith.euclideanHausdorffMeasure_image_setOf_normDet_fderiv_eq_zero.

Sources
LeanLipschitzWith.euclideanHausdorffMeasure_image_setOf_normDet_fderiv_eq_zero

TheoremVitali's convergence theorem for maps into a pseudometric space#

Let 1 ≤ p < ∞, let μ be a finite measure, and let the almost-everywhere measurable maps T n, T₀ : X → Y have finite p-th moment about a point y₀. Then dist (T n x) (T₀ x) tends to 0 in Lᵖ(μ) if and only if T n converges to T₀ in μ-measure and the family dist (T n ·) y₀ is uniformly integrable in Lᵖ(μ).

TauCeti.tendsto_eLpNorm_dist_iff_tendstoInMeasure_and_unifIntegrable.{u_1, u_2} {X : Type u_1}
  {Y : Type u_2} [PseudoMetricSpace Y] [MeasurableSpace X] [MeasurableSpace Y]
  [OpensMeasurableSpace Y] [SecondCountableTopology Y] {μ : MeasureTheory.Measure X} {p : ENNReal}
  [MeasureTheory.IsFiniteMeasure μ] {T : ℕ → X → Y} {T₀ : X → Y} {y₀ : Y} (hp : 1 ≤ p) (hp' : p ≠ ⊤)
  (hT : ∀ (n : ℕ), AEMeasurable (T n) μ) (hT₀ : AEMeasurable T₀ μ)
  (hTp : ∀ (n : ℕ), MeasureTheory.MemLp (fun x => dist (T n x) y₀) p μ)
  (hT₀p : MeasureTheory.MemLp (fun x => dist (T₀ x) y₀) p μ) :
  Filter.Tendsto (fun n => MeasureTheory.eLpNorm (fun x => dist (T n x) (T₀ x)) p μ) Filter.atTop
      (nhds 0) ↔
    MeasureTheory.TendstoInMeasure μ T Filter.atTop T₀ ∧
      MeasureTheory.UnifIntegrable (fun n x => dist (T n x) y₀) p μ
Lean

Formalized in Tau Ceti as TauCeti.tendsto_eLpNorm_dist_iff_tendstoInMeasure_and_unifIntegrable.

Other forms

Vitali's convergence theorem for maps into a pseudometric space, with MeasureTheory.UniformIntegrable. Formalized in Tau Ceti as TauCeti.tendsto_eLpNorm_dist_iff_tendstoInMeasure_and_uniformIntegrable.

TauCeti.tendsto_eLpNorm_dist_iff_tendstoInMeasure_and_uniformIntegrable.{u_1, u_2} {X : Type u_1}
  {Y : Type u_2} [PseudoMetricSpace Y] [MeasurableSpace X] [MeasurableSpace Y]
  [OpensMeasurableSpace Y] [SecondCountableTopology Y] {μ : MeasureTheory.Measure X} {p : ENNReal}
  [MeasureTheory.IsFiniteMeasure μ] {T : ℕ → X → Y} {T₀ : X → Y} {y₀ : Y} (hp : 1 ≤ p) (hp' : p ≠ ⊤)
  (hT : ∀ (n : ℕ), AEMeasurable (T n) μ) (hT₀ : AEMeasurable T₀ μ)
  (hTp : ∀ (n : ℕ), MeasureTheory.MemLp (fun x => dist (T n x) y₀) p μ)
  (hT₀p : MeasureTheory.MemLp (fun x => dist (T₀ x) y₀) p μ) :
  Filter.Tendsto (fun n => MeasureTheory.eLpNorm (fun x => dist (T n x) (T₀ x)) p μ) Filter.atTop
      (nhds 0) ↔
    MeasureTheory.TendstoInMeasure μ T Filter.atTop T₀ ∧
      MeasureTheory.UniformIntegrable (fun n x => dist (T n x) y₀) p μ
Sources
LeanTauCeti.tendsto_eLpNorm_dist_iff_tendstoInMeasure_and_unifIntegrable · TauCeti.tendsto_eLpNorm_dist_iff_tendstoInMeasure_and_uniformIntegrable

TheoremYoung's inequality for an L¹ kernel#

‖h ⋆ f‖_p ≤ ‖h‖₁ ‖f‖_p.

MeasureTheory.Lp.norm_convolutionL_apply_le.{u_1, u_2, u_3} {G : Type u_1} {E : Type u_2} [Group G]
  [TopologicalSpace G] [IsTopologicalGroup G] [MeasurableSpace G] [BorelSpace G]
  {μ : MeasureTheory.Measure G} [NormedAddCommGroup E] [NormedSpace ℝ E] [μ.IsMulLeftInvariant]
  [MeasureTheory.IsLocallyFiniteMeasure μ] [μ.InnerRegularCompactLTTop] {p : ENNReal} [Fact (1 ≤ p)]
  {𝕜 : Type u_3} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [SMulCommClass ℝ 𝕜 E] {hp : p ≠ ⊤}
  (h : ↥(MeasureTheory.Lp 𝕜 1 μ)) (f : ↥(MeasureTheory.Lp E p μ)) :
  ‖((MeasureTheory.Lp.convolutionL μ p hp) h) f‖ ≤ ‖h‖ * ‖f‖
Lean

Formalized in Tau Ceti as MeasureTheory.Lp.norm_convolutionL_apply_le.

Other forms

Young's inequality for convolution with an integrable kernel. Formalized in Tau Ceti as TauCeti.norm_convolutionLp_le.

TauCeti.norm_convolutionLp_le.{u_1, u_2} {E : Type u_1} {F : Type u_2} [MeasurableSpace E]
  [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E]
  [NormedAddCommGroup F] [NormedSpace ℝ F] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure]
  {p : ENNReal} [Fact (1 ≤ p)] (hp : p ≠ ⊤) (k : E → ℝ) :
  ‖TauCeti.convolutionLp hp k μ‖ ≤ ∫ (y : E), ‖k y‖ ∂μ
Sources
LeanMeasureTheory.Lp.norm_convolutionL_apply_le · TauCeti.norm_convolutionLp_le
Used by 1
Used byDuhamel's formula for the heat equation

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.