def Majorizes {Ω : Type u_1} (f g : Ω → ℝ) : Prop

Definition 8.5 (Majorization): for functions f, g : Ω → ℝ, f majorizes g (equivalently, g minorizes f) iff ∀ x : Ω, f x ≥ g x.

Equations

• Majorizes f g = ∀ (x : Ω), f x ≥ g x

noncomputable def integralOver {X : Type u_1} [MeasurableSpace X] (μ : MeasureTheory.Measure X) (Ω : Set X) (f : X → ENNReal) : ENNReal

Integral of a nonnegative function over a set, encoded via an indicator on the ambient space.

Equations

• integralOver μ Ω f = ∫⁻ (x : X), Ω.indicator f x ∂μ

theorem helperForProposition_8_3_1_integralOver_eq_setLIntegral {X : Type u_1} [MeasurableSpace X] (μ : MeasureTheory.Measure X) {Ω : Set X} (hΩ : MeasurableSet Ω) (f : X → ENNReal) : integralOver μ Ω f = ∫⁻ (x : X) in Ω, f x ∂μ

Rewrite the indicator-based set integral as a restricted lintegral.

theorem helperForProposition_8_3_1_setLIntegral_eq_zero_iff_aeOn {X : Type u_1} [MeasurableSpace X] (μ : MeasureTheory.Measure X) {Ω : Set X} (hΩ : MeasurableSet Ω) {f : X → ENNReal} (hf : Measurable f) : ∫⁻ (x : X) in Ω, f x ∂μ = 0 ↔ ∀ᵐ (x : X) ∂μ, x ∈ Ω → f x = 0

A restricted lintegral vanishes iff the function vanishes almost everywhere on the set.

theorem helperForProposition_8_3_1_integralOver_nonneg_le_top {X : Type u_1} [MeasurableSpace X] (μ : MeasureTheory.Measure X) (Ω : Set X) (f : X → ENNReal) : 0 ≤ integralOver μ Ω f ∧ integralOver μ Ω f ≤ ⊤

The integral over a set is bounded between 0 and ⊤.

theorem helperForProposition_8_3_1_aeOn_restrict_bridge {X : Type u_1} [MeasurableSpace X] (μ : MeasureTheory.Measure X) {Ω : Set X} (hΩ : MeasurableSet Ω) (f : X → ENNReal) : (∀ᵐ (x : X) ∂μ.restrict Ω, f x = 0) ↔ ∀ᵐ (x : X) ∂μ, x ∈ Ω → f x = 0

Bridge restricted-measure a.e. and ambient a.e.-on-set formulations.

theorem proposition_8_3_1 {X : Type u_1} [MeasurableSpace X] (μ : MeasureTheory.Measure X) {Ω : Set X} (hΩ : MeasurableSet Ω) {f : X → ENNReal} (hf : Measurable f) : (0 ≤ integralOver μ Ω f ∧ integralOver μ Ω f ≤ ⊤) ∧ (integralOver μ Ω f = 0 ↔ ∀ᵐ (x : X) ∂μ, x ∈ Ω → f x = 0)

Proposition 8.3.1: for a measurable set Ω and measurable f : X → [0, ∞], the indicator-based integral over Ω is in [0, ∞], and it is zero iff f = 0 for μ-almost every x ∈ Ω.

theorem proposition_8_3_2 {X : Type u_1} [MeasurableSpace X] (μ : MeasureTheory.Measure X) {Ω : Set X} (hΩ : MeasurableSet Ω) {f : X → ENNReal} (hf : Measurable f) (c : ENNReal) (hc : 0 < c) : (integralOver μ Ω fun (x : X) => c * f x) = c * integralOver μ Ω f

Proposition 8.3.2: for a measurable set Ω and measurable f : X → [0, ∞], if c > 0 then integrating cf over Ω scales the integral by c.

noncomputable def extendByZero {X : Type u_1} (Ω : Set X) (f : ↑Ω → ENNReal) : X → ENNReal

Extension by zero from Ω to the ambient space.

Equations

• extendByZero Ω f x = if hx : x ∈ Ω then f ⟨x, hx⟩ else 0

theorem proposition_8_3_3 {X : Type u_1} [MeasurableSpace X] (μ : MeasureTheory.Measure X) {Ω : Set X} (hΩ : MeasurableSet Ω) {f g : ↑Ω → ENNReal} (hf : Measurable f) (hg : Measurable g) (hfg : ∀ (x : ↑Ω), f x ≤ g x) : integralOver μ Ω (extendByZero Ω f) ≤ integralOver μ Ω (extendByZero Ω g)

Proposition 8.3.3: if f, g : Ω → [0, ∞] are measurable and f x ≤ g x for all x ∈ Ω, then the indicator-defined integral over Ω is monotone after extending by zero: ∫_Ω f dμ ≤ ∫_Ω g dμ.

theorem helperForProposition_8_3_4_ae_indicator_congr {X : Type u_1} [MeasurableSpace X] (μ : MeasureTheory.Measure X) {Ω : Set X} {u v : X → ENNReal} (huv : ∀ᵐ (x : X) ∂μ, x ∈ Ω → u x = v x) : ∀ᵐ (x : X) ∂μ, Ω.indicator u x = Ω.indicator v x

Helper for Proposition 8.3.4: convert a.e.-on-Ω equality into a.e. equality of indicator integrands.

theorem helperForProposition_8_3_4_integralOver_congr_aeOn {X : Type u_1} [MeasurableSpace X] (μ : MeasureTheory.Measure X) (Ω : Set X) {u v : X → ENNReal} (huv : ∀ᵐ (x : X) ∂μ, x ∈ Ω → u x = v x) : integralOver μ Ω u = integralOver μ Ω v

Helper for Proposition 8.3.4: a.e.-on-Ω equality implies equality of indicator-defined integrals over Ω.

theorem proposition_8_3_4 {X : Type u_1} [MeasurableSpace X] (μ : MeasureTheory.Measure X) {Ω : Set X} (hΩ : MeasurableSet Ω) {f g : ↑Ω → ENNReal} (hf : Measurable f) (hg : Measurable g) (hfg : ∀ᵐ (x : X) ∂μ, x ∈ Ω → extendByZero Ω f x = extendByZero Ω g x) : integralOver μ Ω (extendByZero Ω f) = integralOver μ Ω (extendByZero Ω g)

Proposition 8.3.4: let Ω be measurable and let f, g : Ω → [0, ∞] be measurable. If f = g for μ-almost every x ∈ Ω, then their indicator-defined integrals over Ω are equal.

theorem helperForProposition_8_3_5_indicator_collapse_under_subset {X : Type u_1} {Ω Ω' : Set X} (hΩ'sub : Ω' ⊆ Ω) (u : X → ENNReal) : Ω.indicator (Ω'.indicator u) = Ω'.indicator u

Helper for Proposition 8.3.5: collapsing nested indicators when Ω' ⊆ Ω.

theorem helperForProposition_8_3_5_integralOver_indicator_eq {X : Type u_1} [MeasurableSpace X] (μ : MeasureTheory.Measure X) {Ω Ω' : Set X} (hΩ'sub : Ω' ⊆ Ω) (u : X → ENNReal) : integralOver μ Ω' u = integralOver μ Ω (Ω'.indicator u)

Helper for Proposition 8.3.5: rewriting the Ω'-integral as an Ω-integral of an indicator-restricted integrand.

theorem helperForProposition_8_3_5_integralOver_mono_subset {X : Type u_1} [MeasurableSpace X] (μ : MeasureTheory.Measure X) {Ω Ω' : Set X} (hΩ'sub : Ω' ⊆ Ω) (u : X → ENNReal) : integralOver μ Ω' u ≤ integralOver μ Ω u

Helper for Proposition 8.3.5: monotonicity of integralOver under set inclusion.

theorem proposition_8_3_5 {X : Type u_1} [MeasurableSpace X] (μ : MeasureTheory.Measure X) {Ω Ω' : Set X} (hΩ : MeasurableSet Ω) (hΩ' : MeasurableSet Ω') (hΩ'sub : Ω' ⊆ Ω) {f : ↑Ω → ENNReal} (hf : Measurable f) : integralOver μ Ω' (extendByZero Ω f) = integralOver μ Ω (Ω'.indicator (extendByZero Ω f)) ∧ integralOver μ Ω (Ω'.indicator (extendByZero Ω f)) ≤ integralOver μ Ω (extendByZero Ω f)

Proposition 8.3.5: for measurable Ω' ⊆ Ω and measurable f : Ω → [0, ∞], the integral over Ω' equals the integral over Ω of extendByZero Ω f multiplied by χ_{Ω'}, and this quantity is at most the integral over Ω of extendByZero Ω f.

def IsNonnegativeSimpleFunctionOn {n : ℕ} (Ω : Set (Fin n → ℝ)) (s : (Fin n → ℝ) → ENNReal) : Prop

A non-negative simple function on Ω is a finite sum of non-negative coefficients times indicators of measurable subsets of Ω.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def nonnegativeSimpleFunctionIntegral {n : ℕ} (m : ℕ) (a : Fin m → NNReal) (E : Fin m → Set (Fin n → ℝ)) : ENNReal

Integral formula for a represented non-negative simple function.

Equations

• nonnegativeSimpleFunctionIntegral m a E = ∑ k : Fin m, ↑(a k) * MeasureTheory.volume (E k)

theorem lintegral_eq_nonnegativeSimpleFunctionIntegral {n : ℕ} (Ω : Set (Fin n → ℝ)) (m : ℕ) (a : Fin m → NNReal) (E : Fin m → Set (Fin n → ℝ)) (hE_meas : ∀ (k : Fin m), MeasurableSet (E k)) (hE_sub : ∀ (k : Fin m), E k ⊆ Ω) : ∫⁻ (x : Fin n → ℝ) in Ω, ∑ k : Fin m, ↑(a k) * (E k).indicator (fun (x : Fin n → ℝ) => 1) x = nonnegativeSimpleFunctionIntegral m a E

For a represented simple function, integration over Ω matches the coefficient-measure sum.

noncomputable def lebesgueIntegralNonnegSup {n : ℕ} (Ω : Set (Fin n → ℝ)) (f : (Fin n → ℝ) → ENNReal) : ENNReal

Supremum over non-negative simple functions bounded above by f on Ω.

Equations

• lebesgueIntegralNonnegSup Ω f = ⨆ (s : (Fin n → ℝ) → ENNReal), ⨆ (_ : IsNonnegativeSimpleFunctionOn Ω s), ⨆ (_ : ∀ x ∈ Ω, s x ≤ f x), ∫⁻ (x : Fin n → ℝ) in Ω, s x

noncomputable def lebesgueIntegralNonneg {n : ℕ} (Ω : Set (Fin n → ℝ)) (f : (Fin n → ℝ) → ENNReal) : ENNReal

Definition 8.6 (Lebesgue integral for non-negative functions): define ∫_Ω f dx by the restricted Lebesgue integral.

Equations

• lebesgueIntegralNonneg Ω f = ∫⁻ (x : Fin n → ℝ) in Ω, f x

theorem lintegral_add_on_measurableSet_subtype {n : ℕ} {Ω : Set (Fin n → ℝ)} (hΩ : MeasurableSet Ω) {f g : ↑Ω → ENNReal} (hf : Measurable f) (hg : Measurable g) : ∫⁻ (x : ↑Ω), f x + g x ∂MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume = ∫⁻ (x : ↑Ω), f x ∂MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume + ∫⁻ (x : ↑Ω), g x ∂MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume

Lemma 8.5 (Interchange of addition and integration): if Ω ⊆ ℝ^n is measurable and f, g : Ω → [0, ∞] are measurable, then integrating f + g over Ω equals the sum of the integrals of f and g over Ω.

theorem lintegral_liminf_le_liminf_lintegral_subtype {n : ℕ} {Ω : Set (Fin n → ℝ)} (hΩ : MeasurableSet Ω) (f : ℕ → ↑Ω → ENNReal) (hf : ∀ (k : ℕ), Measurable (f k)) : ∫⁻ (x : ↑Ω), Filter.liminf (fun (k : ℕ) => f k x) Filter.atTop ∂MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume ≤ Filter.liminf (fun (k : ℕ) => ∫⁻ (x : ↑Ω), f k x ∂MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume) Filter.atTop

Lemma 8.6 (Fatou's lemma): if Ω ⊆ ℝ^n is measurable and f_n : Ω → [0, ∞] is measurable for each n, then ∫_Ω liminf_{n→∞} f_n ≤ liminf_{n→∞} ∫_Ω f_n.

theorem isNonnegativeSimpleFunctionOn_eq_zero_outside {n : ℕ} {Ω : Set (Fin n → ℝ)} {s : (Fin n → ℝ) → ENNReal} (hs : IsNonnegativeSimpleFunctionOn Ω s) (x : Fin n → ℝ) : x ∉ Ω → s x = 0

A non-negative simple function on Ω vanishes outside Ω.

theorem lintegral_le_of_isNonnegativeSimpleFunctionOn_minorized {n : ℕ} {Ω : Set (Fin n → ℝ)} {f s : (Fin n → ℝ) → ENNReal} (hs : IsNonnegativeSimpleFunctionOn Ω s) (hdom : ∀ x ∈ Ω, s x ≤ f x) : ∫⁻ (x : Fin n → ℝ) in Ω, s x ≤ ∫⁻ (x : Fin n → ℝ) in Ω, f x

An admissible non-negative simple minorant is bounded by the restricted integral of f.

theorem isNonnegativeSimpleFunctionOn_of_restricted_nnreal_simpleFunc {n : ℕ} {Ω t : Set (Fin n → ℝ)} (ht : MeasurableSet t) (htΩ : t ⊆ Ω) (φ : MeasureTheory.SimpleFunc (Fin n → ℝ) NNReal) : IsNonnegativeSimpleFunctionOn Ω fun (x : Fin n → ℝ) => (MeasureTheory.SimpleFunc.map ENNReal.ofNNReal (φ.restrict t)) x

Restricting an NNReal simple function to measurable t ⊆ Ω yields an admissible non-negative simple function on Ω after coercion to ENNReal.

theorem lebesgueIntegralNonneg_eq_iSup_simple {n : ℕ} (Ω : Set (Fin n → ℝ)) (f : (Fin n → ℝ) → ENNReal) (hΩ : MeasureTheory.NullMeasurableSet Ω MeasureTheory.volume) (hf : AEMeasurable f (MeasureTheory.volume.restrict Ω)) : lebesgueIntegralNonneg Ω f = lebesgueIntegralNonnegSup Ω f

Under measurability assumptions on Ω and f, the restricted lintegral agrees with the supremum over non-negative simple functions bounded by f on Ω.

theorem helperForTheorem_8_1_subtypeIntegral_repr {n : ℕ} {Ω : Set (Fin n → ℝ)} (hΩ : MeasurableSet Ω) (g : (Fin n → ℝ) → ENNReal) : lebesgueIntegralNonneg Ω g = ∫⁻ (x : ↑Ω), g ↑x ∂MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume

Helper for Theorem 8.1: rewrite lebesgueIntegralNonneg as a subtype-domain integral.

theorem helperForTheorem_8_1_subtypePointwiseMonotone {n : ℕ} {Ω : Set (Fin n → ℝ)} (f : ℕ → (Fin n → ℝ) → ENNReal) (hmono : ∀ x ∈ Ω, Monotone fun (k : ℕ) => f k x) : Monotone fun (k : ℕ) (x : ↑Ω) => f k ↑x

Helper for Theorem 8.1: pointwise monotonicity on Ω as monotonicity over the subtype.

theorem helperForTheorem_8_1_subtypeIntegral_monotone {n : ℕ} {Ω : Set (Fin n → ℝ)} (f : ℕ → (Fin n → ℝ) → ENNReal) (hmono : ∀ x ∈ Ω, Monotone fun (k : ℕ) => f k x) : Monotone fun (k : ℕ) => ∫⁻ (x : ↑Ω), f k ↑x ∂MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume

Helper for Theorem 8.1: monotonicity of subtype integrals for a pointwise monotone sequence.

theorem helperForTheorem_8_1_subtype_mct_identity {n : ℕ} {Ω : Set (Fin n → ℝ)} (f : ℕ → (Fin n → ℝ) → ENNReal) (hf_meas : ∀ (n_1 : ℕ), Measurable fun (x : ↑Ω) => f n_1 ↑x) (hmono : ∀ x ∈ Ω, Monotone fun (k : ℕ) => f k x) : ∫⁻ (x : ↑Ω), ⨆ (k : ℕ), f k ↑x ∂MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume = ⨆ (k : ℕ), ∫⁻ (x : ↑Ω), f k ↑x ∂MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume

Helper for Theorem 8.1: subtype-domain monotone convergence identity.

theorem lebesgue_monotone_convergence {n : ℕ} {Ω : Set (Fin n → ℝ)} (hΩ : MeasurableSet Ω) (f : ℕ → (Fin n → ℝ) → ENNReal) (hf_meas : ∀ (n_1 : ℕ), Measurable fun (x : ↑Ω) => f n_1 ↑x) (hmono : ∀ x ∈ Ω, Monotone fun (n : ℕ) => f n x) : (0 ≤ lebesgueIntegralNonneg Ω (f 0) ∧ Monotone fun (n_1 : ℕ) => lebesgueIntegralNonneg Ω (f n_1)) ∧ (lebesgueIntegralNonneg Ω fun (x : Fin n → ℝ) => ⨆ (n : ℕ), f n x) = ⨆ (n_1 : ℕ), lebesgueIntegralNonneg Ω (f n_1)

Theorem 8.1 (Lebesgue monotone convergence theorem): if Ω ⊆ ℝ^n is measurable and f : ℕ → (Fin n → ℝ) → ENNReal is pointwise monotone on Ω (so f 0, f 1, ... models f₁, f₂, ...), then the restricted integrals are monotone and ∫_Ω (⨆ n, f n) = ⨆ n, ∫_Ω f n.

theorem helperForTheorem_8_2_shiftedFamily_measurable {n : ℕ} {Ω : Set (Fin n → ℝ)} (g : ℕ → ↑Ω → ENNReal) (hg : ∀ (k : ℕ), Measurable (g (k + 1))) (k : ℕ) : Measurable fun (x : ↑Ω) => g (k + 1) x

Helper for Theorem 8.2: each shifted term x ↦ g (k + 1) x is measurable.

theorem helperForTheorem_8_2_tsum_measurable {n : ℕ} {Ω : Set (Fin n → ℝ)} (g : ℕ → ↑Ω → ENNReal) (hg : ∀ (k : ℕ), Measurable (g (k + 1))) : Measurable fun (x : ↑Ω) => ∑' (k : ℕ), g (k + 1) x

Helper for Theorem 8.2: the shifted pointwise series is measurable.

theorem helperForTheorem_8_2_shiftedFamily_aemeasurable {n : ℕ} {Ω : Set (Fin n → ℝ)} (g : ℕ → ↑Ω → ENNReal) (hg : ∀ (k : ℕ), Measurable (g (k + 1))) (k : ℕ) : AEMeasurable (fun (x : ↑Ω) => g (k + 1) x) (MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume)

Helper for Theorem 8.2: each shifted term is a.e.-measurable for the subtype measure.

theorem helperForTheorem_8_2_lintegral_tsum {n : ℕ} {Ω : Set (Fin n → ℝ)} (g : ℕ → ↑Ω → ENNReal) (hg : ∀ (k : ℕ), Measurable (g (k + 1))) : ∫⁻ (x : ↑Ω), ∑' (k : ℕ), g (k + 1) x ∂MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume = ∑' (k : ℕ), ∫⁻ (x : ↑Ω), g (k + 1) x ∂MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume

Helper for Theorem 8.2: lintegral of the shifted series equals the series of lintegrals.

theorem lintegral_tsum_subtype_eq_tsum_lintegral_subtype {n : ℕ} {Ω : Set (Fin n → ℝ)} (hΩ : MeasurableSet Ω) (g : ℕ → ↑Ω → ENNReal) (hg : ∀ (k : ℕ), Measurable (g (k + 1))) : (Measurable fun (x : ↑Ω) => ∑' (k : ℕ), g (k + 1) x) ∧ ∫⁻ (x : ↑Ω), ∑' (k : ℕ), g (k + 1) x ∂MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume = ∑' (k : ℕ), ∫⁻ (x : ↑Ω), g (k + 1) x ∂MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume

Theorem 8.2: for a measurable set Ω ⊆ ℝ^n and measurable g_n : Ω → [0,∞], define G(x) = ∑' n, g (n + 1) x (series indexed by n ≥ 1). Then G is measurable and integrating G over Ω equals the sum of the integrals of the g_n, with values in [0,∞].

theorem proposition_8_4_ae_lt_top_of_lintegral_lt_top {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) {f : Ω → ENNReal} (hf : Measurable f) (hfin : ∫⁻ (ω : Ω), f ω ∂μ < ⊤) : ∀ᵐ (ω : Ω) ∂μ, f ω < ⊤

Proposition 8.4: for a measure space (Ω, 𝓕, μ) and a measurable function f : Ω → [0, +∞], if ∫⁻ ω, f ω ∂μ < +∞, then f ω < +∞ for μ-almost every ω.

theorem lemma_8_7_ae_lt_top_on_measurable_set {n : ℕ} {Ω : Set (Fin n → ℝ)} (hΩ : MeasurableSet Ω) {f : ↑Ω → ENNReal} (hf : Measurable f) (hfin : ∫⁻ (x : ↑Ω), f x ∂MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume < ⊤) : ∀ᵐ (x : ↑Ω) ∂MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume, f x < ⊤

Lemma 8.7: if Ω ⊆ ℝ^n is measurable and f : Ω → [0, +∞] is measurable with ∫_Ω f dx < +∞, then f x < +∞ for almost every x ∈ Ω (equivalently, |{x ∈ Ω : f x = +∞}| = 0).

theorem proposition_8_5_lintegral_add_ge {n : ℕ} {Ω : Set (Fin n → ℝ)} (hΩ : MeasurableSet Ω) {f g : ↑Ω → ENNReal} (hf : Measurable f) (hg : Measurable g) : ∫⁻ (x : ↑Ω), f x + g x ∂MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume ≥ ∫⁻ (x : ↑Ω), f x ∂MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume + ∫⁻ (x : ↑Ω), g x ∂MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume

Proposition 8.5: if Ω ⊆ ℝ^n is measurable and f, g : Ω → [0,+∞] are measurable, then ∫ (f + g) ≥ ∫ f + ∫ g over Ω (with respect to Lebesgue measure on the subtype).

theorem lemma_8_8_borel_cantelli {n : ℕ} (Ω : ℕ → Set (Fin n → ℝ)) (hmeas : ∀ (k : ℕ), MeasurableSet (Ω k)) (hsum : ∑' (k : ℕ), MeasureTheory.volume (Ω k) < ⊤) : MeasureTheory.volume (⋂ (N : ℕ), ⋃ (k : ℕ), ⋃ (_ : k ≥ N), Ω k) = 0

Lemma 8.8 (Borel--Cantelli): for measurable sets Ω₁, Ω₂, ... ⊆ ℝ^n, if ∑' k, volume (Ω k) < ∞, then the limsup set ⋂ N, ⋃ k ≥ N, Ω k has Lebesgue measure zero.

theorem helperForProposition_8_6_rational_of_exists_exact_ratio {x : ℝ} (h : ∃ (aq : ℕ × ℕ), 0 < aq.2 ∧ x = ↑aq.1 / ↑aq.2) : x ∈ Set.range Rat.cast

Helper for Proposition 8.6: exact equality with a positive-denominator natural ratio gives a rational real.

theorem helperForProposition_8_6_finite_pairs_if_denominator_bounded {p c x : ℝ} (hp : 2 < p) (hc : 0 < c) (hx01 : x ∈ Set.Icc 0 1) {N : ℕ} : {aq : ℕ × ℕ | 0 < aq.1 ∧ 0 < aq.2 ∧ aq.2 ≤ N ∧ |x - ↑aq.1 / ↑aq.2| ≤ c / ↑aq.2 ^ p}.Finite

Helper for Proposition 8.6: for x ∈ [0,1], admissible pairs with denominator bounded by N form a finite set.

theorem helperForProposition_8_6_liouvilleWith_of_infinite_pairs_nonrational {p c x : ℝ} (hp : 2 < p) (hc : 0 < c) (hx01 : x ∈ Set.Icc 0 1) (hx_nonrat : x ∉ Set.range Rat.cast) (hInf : {aq : ℕ × ℕ | 0 < aq.1 ∧ 0 < aq.2 ∧ |x - ↑aq.1 / ↑aq.2| ≤ c / ↑aq.2 ^ p}.Infinite) : LiouvilleWith p x

Helper for Proposition 8.6: for nonrational x ∈ [0,1], infinitely many admissible pairs imply LiouvilleWith p x.

theorem helperForProposition_8_6_volume_setOf_liouvilleWith_zero {p : ℝ} (hp : 2 < p) : MeasureTheory.volume {x : ℝ | LiouvilleWith p x} = 0

Helper for Proposition 8.6: the fixed-exponent Liouville set has measure zero when p > 2.

theorem proposition_8_6_measure_zero_of_infinitely_many_rational_approximations {p c : ℝ} (hp : 2 < p) (hc : 0 < c) : MeasureTheory.volume {x : ℝ | x ∈ Set.Icc 0 1 ∧ {aq : ℕ × ℕ | 0 < aq.1 ∧ 0 < aq.2 ∧ |x - ↑aq.1 / ↑aq.2| ≤ c / ↑aq.2 ^ p}.Infinite} = 0

Proposition 8.6: let p > 2 and c > 0, and define E = {x ∈ [0,1] : |x - a / q| ≤ c / q^p for infinitely many positive integer pairs (a,q)}. Then E has Lebesgue measure zero.

def helperForTheorem_8_3_diophantineExponent (τ x : ℝ) : Prop

Helper for Theorem 8.3: x has a uniform Diophantine lower bound with exponent τ over positive natural denominators.

Equations

• helperForTheorem_8_3_diophantineExponent τ x = ∃ (c : ℝ), 0 < c ∧ ∀ (p : ℤ) (q : ℕ), 0 < q → |x - ↑p / ↑q| ≥ c / ↑q ^ τ

theorem helperForTheorem_8_3_monotone_in_exponent {τ τ' x : ℝ} (hτ : τ ≤ τ') : helperForTheorem_8_3_diophantineExponent τ x → helperForTheorem_8_3_diophantineExponent τ' x

Helper for Theorem 8.3: increasing the exponent preserves the Diophantine lower-bound property.

theorem helperForTheorem_8_3_monotone_in_exponent_add_nonneg {τ δ x : ℝ} (hδ : 0 ≤ δ) : helperForTheorem_8_3_diophantineExponent τ x → helperForTheorem_8_3_diophantineExponent (τ + δ) x

Helper for Theorem 8.3: adding a nonnegative increment to the exponent preserves the Diophantine lower-bound property.

theorem helperForTheorem_8_3_diophantineExponent_succ {τ x : ℝ} : helperForTheorem_8_3_diophantineExponent τ x → helperForTheorem_8_3_diophantineExponent (τ + 1) x

Helper for Theorem 8.3: a Diophantine lower bound at exponent τ also gives one at exponent τ + 1.

theorem helperForTheorem_8_3_monotone_in_exponent_strict {τ τ' x : ℝ} (hτ : τ < τ') : helperForTheorem_8_3_diophantineExponent τ x → helperForTheorem_8_3_diophantineExponent τ' x

Helper for Theorem 8.3: strict exponent increase preserves the Diophantine lower-bound property.

theorem helperForTheorem_8_3_diophantineExponent_iff_denominator_ne_zero {τ x : ℝ} : helperForTheorem_8_3_diophantineExponent τ x ↔ ∃ (c : ℝ), 0 < c ∧ ∀ (p : ℤ) (q : ℕ), q ≠ 0 → |x - ↑p / ↑q| ≥ c / ↑q ^ τ

Helper for Theorem 8.3: for natural denominators, the side condition 0 < q is equivalent to q ≠ 0 in the Diophantine exponent formulation.

theorem helperForTheorem_8_3_diophantineExponent_strict_of_non_strict {τ x : ℝ} : helperForTheorem_8_3_diophantineExponent τ x → ∃ (c : ℝ), 0 < c ∧ ∀ (p : ℤ) (q : ℕ), 0 < q → |x - ↑p / ↑q| > c / ↑q ^ τ

Helper for Theorem 8.3: a non-strict Diophantine lower bound can be upgraded to a strict lower bound by shrinking the constant.

def IsDiophantineReal (x : ℝ) : Prop

Definition 8.7: a real number x is diophantine if there exist constants p > 0 and C > 0 such that |x - a/q| > C / |q|^p for every nonzero integer q and every integer a.

Equations

• IsDiophantineReal x = ∃ (p : ℝ) (C : ℝ), 0 < p ∧ 0 < C ∧ ∀ (q : ℤ), q ≠ 0 → ∀ (a : ℤ), |x - ↑a / ↑q| > C / ↑q.natAbs ^ p

theorem helperForTheorem_8_3_exists_non_strict_parameters_of_IsDiophantineReal {x : ℝ} (hx : IsDiophantineReal x) : ∃ (p : ℝ) (C : ℝ), 0 < p ∧ 0 < C ∧ ∀ (q : ℤ), q ≠ 0 → ∀ (a : ℤ), |x - ↑a / ↑q| ≥ C / ↑q.natAbs ^ p

Helper for Theorem 8.3: strict integer-denominator Diophantine bounds imply the corresponding non-strict bounds.

theorem helperForTheorem_8_3_isDiophantineReal_of_exists_non_strict_parameters {x : ℝ} (hx : ∃ (p : ℝ) (C : ℝ), 0 < p ∧ 0 < C ∧ ∀ (q : ℤ), q ≠ 0 → ∀ (a : ℤ), |x - ↑a / ↑q| ≥ C / ↑q.natAbs ^ p) : IsDiophantineReal x

Helper for Theorem 8.3: non-strict integer-denominator Diophantine bounds imply IsDiophantineReal after shrinking the constant.

theorem helperForTheorem_8_3_isDiophantineReal_iff_exists_non_strict_parameters {x : ℝ} : IsDiophantineReal x ↔ ∃ (p : ℝ) (C : ℝ), 0 < p ∧ 0 < C ∧ ∀ (q : ℤ), q ≠ 0 → ∀ (a : ℤ), |x - ↑a / ↑q| ≥ C / ↑q.natAbs ^ p

Helper for Theorem 8.3: IsDiophantineReal is equivalent to the existence of positive-parameter non-strict integer-denominator Diophantine bounds.

theorem helperForTheorem_8_3_signed_numerator_div_natAbs_eq_div_int (a q : ℤ) (hq : q ≠ 0) : ↑(a * q.sign) / ↑q.natAbs = ↑a / ↑q

Helper for Theorem 8.3: rewrite an integer-denominator rational into a positive-denominator one using Int.sign and Int.natAbs.

theorem helperForTheorem_8_3_exists_exponent_with_diophantineExponent_of_IsDiophantineReal {x : ℝ} (hx : IsDiophantineReal x) : ∃ (τ : ℝ), 0 < τ ∧ helperForTheorem_8_3_diophantineExponent τ x

Helper for Theorem 8.3: an IsDiophantineReal number satisfies the natural-denominator Diophantine lower-bound formulation at some positive exponent.

theorem helperForTheorem_8_3_isDiophantineReal_of_diophantineExponent {x τ : ℝ} (hτ : 0 < τ) (hx : helperForTheorem_8_3_diophantineExponent τ x) : IsDiophantineReal x

Helper for Theorem 8.3: a positive-exponent natural-denominator Diophantine lower bound implies IsDiophantineReal.

theorem helperForTheorem_8_3_isDiophantineReal_of_diophantineExponent_gt_one {x τ : ℝ} (hτ : 1 < τ) (hx : helperForTheorem_8_3_diophantineExponent τ x) : IsDiophantineReal x

Helper for Theorem 8.3: a natural-denominator Diophantine lower bound at an exponent strictly greater than 1 implies IsDiophantineReal.

theorem helperForTheorem_8_3_isDiophantineReal_iff_exists_positive_exponent {x : ℝ} : IsDiophantineReal x ↔ ∃ (τ : ℝ), 0 < τ ∧ helperForTheorem_8_3_diophantineExponent τ x

Helper for Theorem 8.3: the integer-denominator and positive-natural-denominator Diophantine formulations are equivalent.

theorem helperForTheorem_8_3_exists_exponent_gt_one_of_IsDiophantineReal {x : ℝ} (hx : IsDiophantineReal x) : ∃ (τ : ℝ), 1 < τ ∧ helperForTheorem_8_3_diophantineExponent τ x

Helper for Theorem 8.3: any IsDiophantineReal number admits a natural-denominator Diophantine lower bound at some exponent strictly greater than 1.

theorem helperForTheorem_8_3_isDiophantineReal_of_exists_exponent_gt_one {x : ℝ} (hx : ∃ (τ : ℝ), 1 < τ ∧ helperForTheorem_8_3_diophantineExponent τ x) : IsDiophantineReal x

Helper for Theorem 8.3: existence of a strict-> 1 natural-denominator Diophantine lower bound implies IsDiophantineReal.

theorem helperForTheorem_8_3_isDiophantineReal_iff_exists_exponent_gt_one {x : ℝ} : IsDiophantineReal x ↔ ∃ (τ : ℝ), 1 < τ ∧ helperForTheorem_8_3_diophantineExponent τ x

Helper for Theorem 8.3: IsDiophantineReal is equivalent to existence of a natural-denominator Diophantine lower bound at an exponent > 1.

theorem helperForTheorem_8_3_ae_exists_exponent_gt_one_of_ae_isDiophantineReal (hae : ∀ᵐ (x : ℝ), IsDiophantineReal x) : ∀ᵐ (x : ℝ), ∃ (τ : ℝ), 1 < τ ∧ helperForTheorem_8_3_diophantineExponent τ x

Helper for Theorem 8.3: if IsDiophantineReal holds almost everywhere, then almost every point admits an exponent τ > 1 with a natural-denominator Diophantine lower bound.

theorem helperForTheorem_8_3_ae_isDiophantineReal_of_ae_exists_exponent_gt_one (hae : ∀ᵐ (x : ℝ), ∃ (τ : ℝ), 1 < τ ∧ helperForTheorem_8_3_diophantineExponent τ x) : ∀ᵐ (x : ℝ), IsDiophantineReal x

Helper for Theorem 8.3: if almost every point admits an exponent τ > 1 with a natural-denominator Diophantine lower bound, then IsDiophantineReal holds almost everywhere.

theorem helperForTheorem_8_3_ae_isDiophantineReal_iff_ae_exists_exponent_gt_one : (∀ᵐ (x : ℝ), IsDiophantineReal x) ↔ ∀ᵐ (x : ℝ), ∃ (τ : ℝ), 1 < τ ∧ helperForTheorem_8_3_diophantineExponent τ x

Helper for Theorem 8.3: almost-everywhere IsDiophantineReal is equivalent to almost-everywhere existence of an exponent τ > 1 with the natural-denominator Diophantine lower bound.

theorem helperForTheorem_8_3_isDiophantineReal_iff_exists_exponent_gt_one_and_constant {x : ℝ} : IsDiophantineReal x ↔ ∃ (τ : ℝ) (c : ℝ), 1 < τ ∧ 0 < c ∧ ∀ (p : ℤ) (q : ℕ), 0 < q → |x - ↑p / ↑q| ≥ c / ↑q ^ τ

Helper for Theorem 8.3: IsDiophantineReal is equivalent to the existence of an exponent τ > 1 and a constant c > 0 giving the natural-denominator lower bound.

theorem helperForTheorem_8_3_isDiophantineReal_iff_exists_exponent_gt_one_and_constant_ne_zero {x : ℝ} : IsDiophantineReal x ↔ ∃ (τ : ℝ) (c : ℝ), 1 < τ ∧ 0 < c ∧ ∀ (p : ℤ) (q : ℕ), q ≠ 0 → |x - ↑p / ↑q| ≥ c / ↑q ^ τ

Helper for Theorem 8.3: IsDiophantineReal is equivalent to an exponent τ > 1 and a constant c > 0 with the lower bound quantified over all nonzero natural denominators.

theorem helperForTheorem_8_3_ae_iff_volume_complement_zero {τ : ℝ} : (∀ᵐ (x : ℝ), helperForTheorem_8_3_diophantineExponent τ x) ↔ MeasureTheory.volume {x : ℝ | ¬helperForTheorem_8_3_diophantineExponent τ x} = 0

Helper for Theorem 8.3: for Lebesgue measure on ℝ, an almost-everywhere Diophantine lower bound is equivalent to the complement having measure zero.

theorem helperForTheorem_8_3_ae_of_volume_complement_zero {τ : ℝ} (hnull : MeasureTheory.volume {x : ℝ | ¬helperForTheorem_8_3_diophantineExponent τ x} = 0) : ∀ᵐ (x : ℝ), helperForTheorem_8_3_diophantineExponent τ x

Helper for Theorem 8.3: measure-zero complement implies the almost-everywhere Diophantine lower bound formulation.

theorem helperForTheorem_8_3_volume_complement_zero_of_ae {τ : ℝ} (hae : ∀ᵐ (x : ℝ), helperForTheorem_8_3_diophantineExponent τ x) : MeasureTheory.volume {x : ℝ | ¬helperForTheorem_8_3_diophantineExponent τ x} = 0

Helper for Theorem 8.3: an almost-everywhere fixed-exponent Diophantine lower bound implies the complement has Lebesgue measure zero.

theorem helperForTheorem_8_3_full_measure_pair_of_volume_complement_zero {τ : ℝ} (hnull : MeasureTheory.volume {x : ℝ | ¬helperForTheorem_8_3_diophantineExponent τ x} = 0) : MeasureTheory.volume {x : ℝ | ¬helperForTheorem_8_3_diophantineExponent τ x} = 0 ∧ ∀ᵐ (x : ℝ), helperForTheorem_8_3_diophantineExponent τ x

Helper for Theorem 8.3: a null complement yields both the null-complement and almost-everywhere formulations in one conjunction.

theorem helperForTheorem_8_3_full_measure_pair_iff_volume_complement_zero {τ : ℝ} : (MeasureTheory.volume {x : ℝ | ¬helperForTheorem_8_3_diophantineExponent τ x} = 0 ∧ ∀ᵐ (x : ℝ), helperForTheorem_8_3_diophantineExponent τ x) ↔ MeasureTheory.volume {x : ℝ | ¬helperForTheorem_8_3_diophantineExponent τ x} = 0

Helper for Theorem 8.3: proving the full-measure pair is equivalent to proving just the null-complement statement.