ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>inst✝ : LinearOrder α<VAR>a b : α<VAR>h : a ≤ b<GOAL>∀ {d : α}, d ≤ a → d ≤ b → d ≤ a
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G α<VAR>inst✝ : DecidableEq α<VAR>x y z : α<VAR>h : z ∈ {x, y}ᶜ<GOAL>z ∈ fixedBy α (swap x y)
<VAR>α : Type u_1<VAR>inst✝² : OrderedRing α<VAR>inst✝¹ : LocallyFiniteOrder α<VAR>inst✝ : DecidableEq α<VAR>n : ℕ<GOAL>0 ∈ box n ↔ n = 0
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : μ.HaveLebesgueDecomposition ν<VAR>hμν : μ ≪ ν<VAR>c : ℝ≥0∞<VAR>hc : c ≠ 0<VAR>hc_ne_top : c ≠ ⊤<GOAL>llr μ (c • ν) =ᶠ[ae μ] fun x => llr μ ν x - log c.toReal
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : μ.HaveLebesgueDecomposition ν<VAR>hμν : μ ≪ ν<VAR>c : ℝ≥0∞<VAR>hc : c ≠ 0<VAR>hc_ne_top : c ≠ ⊤<GOAL>(fun x => log (μ.rnDeriv (c • ν) x).toReal) =ᶠ[ae μ] fun x => log (μ.rnDeriv ν x).toReal - log c.toReal
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : μ.HaveLebesgueDecomposition ν<VAR>hμν : μ ≪ ν<VAR>c : ℝ≥0∞<VAR>hc : c ≠ 0<VAR>hc_ne_top : c ≠ ⊤<VAR>h : μ.rnDeriv (c • ν) =ᶠ[ae ν] c⁻¹ • μ.rnDeriv ν<GOAL>(fun x => log (μ.rnDeriv (c • ν) x).toReal) =ᶠ[ae μ] fun x => log (μ.rnDeriv ν x).toReal - log c.toReal
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : μ.HaveLebesgueDecomposition ν<VAR>hμν : μ ≪ ν<VAR>c : ℝ≥0∞<VAR>hc : c ≠ 0<VAR>hc_ne_top : c ≠ ⊤<VAR>h : μ.rnDeriv (c • ν) =ᶠ[ae ν] c⁻¹ • μ.rnDeriv ν<VAR>x : α<VAR>hx_eq : μ.rnDeriv (c • ν) x = (c⁻¹ • μ.rnDeriv ν) x<VAR>hx_pos : 0 < μ.rnDeriv ν x<VAR>hx_ne_top : μ.rnDeriv ν x < ⊤<GOAL>log (μ.rnDeriv (c • ν) x).toReal = log (μ.rnDeriv ν x).toReal - log c.toReal
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : μ.HaveLebesgueDecomposition ν<VAR>hμν : μ ≪ ν<VAR>c : ℝ≥0∞<VAR>hc : c ≠ 0<VAR>hc_ne_top : c ≠ ⊤<VAR>h : μ.rnDeriv (c • ν) =ᶠ[ae ν] c⁻¹ • μ.rnDeriv ν<VAR>x : α<VAR>hx_eq : μ.rnDeriv (c • ν) x = (c⁻¹ • μ.rnDeriv ν) x<VAR>hx_pos : 0 < μ.rnDeriv ν x<VAR>hx_ne_top : μ.rnDeriv ν x < ⊤<GOAL>log ((c⁻¹ • μ.rnDeriv ν) x).toReal = log (μ.rnDeriv ν x).toReal - log c.toReal
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : μ.HaveLebesgueDecomposition ν<VAR>hμν : μ ≪ ν<VAR>c : ℝ≥0∞<VAR>hc : c ≠ 0<VAR>hc_ne_top : c ≠ ⊤<VAR>h : μ.rnDeriv (c • ν) =ᶠ[ae ν] c⁻¹ • μ.rnDeriv ν<VAR>x : α<VAR>hx_eq : μ.rnDeriv (c • ν) x = (c⁻¹ • μ.rnDeriv ν) x<VAR>hx_pos : 0 < μ.rnDeriv ν x<VAR>hx_ne_top : μ.rnDeriv ν x < ⊤<GOAL>log (c⁻¹.toReal * (μ.rnDeriv ν x).toReal) = log (μ.rnDeriv ν x).toReal - log c.toReal
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : μ.HaveLebesgueDecomposition ν<VAR>hμν : μ ≪ ν<VAR>c : ℝ≥0∞<VAR>hc : c ≠ 0<VAR>hc_ne_top : c ≠ ⊤<VAR>h : μ.rnDeriv (c • ν) =ᶠ[ae ν] c⁻¹ • μ.rnDeriv ν<VAR>x : α<VAR>hx_eq : μ.rnDeriv (c • ν) x = (c⁻¹ • μ.rnDeriv ν) x<VAR>hx_pos : 0 < μ.rnDeriv ν x<VAR>hx_ne_top : μ.rnDeriv ν x < ⊤<GOAL>log c⁻¹.toReal + log (μ.rnDeriv ν x).toReal = log (μ.rnDeriv ν x).toReal - log c.toReal
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : μ.HaveLebesgueDecomposition ν<VAR>hμν : μ ≪ ν<VAR>c : ℝ≥0∞<VAR>hc : c ≠ 0<VAR>hc_ne_top : c ≠ ⊤<VAR>h : μ.rnDeriv (c • ν) =ᶠ[ae ν] c⁻¹ • μ.rnDeriv ν<VAR>x : α<VAR>hx_eq : μ.rnDeriv (c • ν) x = (c⁻¹ • μ.rnDeriv ν) x<VAR>hx_pos : 0 < μ.rnDeriv ν x<VAR>hx_ne_top : μ.rnDeriv ν x < ⊤<GOAL>c⁻¹.toReal ≠ 0
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : μ.HaveLebesgueDecomposition ν<VAR>hμν : μ ≪ ν<VAR>c : ℝ≥0∞<VAR>hc : c ≠ 0<VAR>hc_ne_top : c ≠ ⊤<VAR>h : μ.rnDeriv (c • ν) =ᶠ[ae ν] c⁻¹ • μ.rnDeriv ν<VAR>x : α<VAR>hx_eq : μ.rnDeriv (c • ν) x = (c⁻¹ • μ.rnDeriv ν) x<VAR>hx_pos : 0 < μ.rnDeriv ν x<VAR>hx_ne_top : μ.rnDeriv ν x < ⊤<GOAL>(μ.rnDeriv ν x).toReal ≠ 0
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : μ.HaveLebesgueDecomposition ν<VAR>hμν : μ ≪ ν<VAR>c : ℝ≥0∞<VAR>hc : c ≠ 0<VAR>hc_ne_top : c ≠ ⊤<VAR>h : μ.rnDeriv (c • ν) =ᶠ[ae ν] c⁻¹ • μ.rnDeriv ν<VAR>x : α<VAR>hx_eq : μ.rnDeriv (c • ν) x = (c⁻¹ • μ.rnDeriv ν) x<VAR>hx_pos : 0 < μ.rnDeriv ν x<VAR>hx_ne_top : μ.rnDeriv ν x < ⊤<GOAL>-log c.toReal + log (μ.rnDeriv ν x).toReal = log (μ.rnDeriv ν x).toReal - log c.toReal
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>R : ℝ≥0<VAR>inst✝ : IsFiniteMeasure μ<VAR>g : Ω → ℝ<VAR>hg : Integrable g μ<VAR>hgmeas : StronglyMeasurable g<GOAL>∀ᵐ (x : Ω) ∂μ, Tendsto (fun n => (μ[g|↑ℱ n]) x) atTop (𝓝 (g x))
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>R : ℝ≥0<VAR>inst✝ : IsFiniteMeasure μ<VAR>g : Ω → ℝ<VAR>hg : Integrable g μ<VAR>hgmeas : StronglyMeasurable g<VAR>hle : ⨆ n, ↑ℱ n ≤ m0<GOAL>∀ᵐ (x : Ω) ∂μ, Tendsto (fun n => (μ[g|↑ℱ n]) x) atTop (𝓝 (g x))
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>R : ℝ≥0<VAR>inst✝ : IsFiniteMeasure μ<VAR>g : Ω → ℝ<VAR>hg : Integrable g μ<VAR>hgmeas : StronglyMeasurable g<VAR>hle : ⨆ n, ↑ℱ n ≤ m0<VAR>hunif : UniformIntegrable (fun n => μ[g|↑ℱ n]) 1 μ<GOAL>∀ᵐ (x : Ω) ∂μ, Tendsto (fun n => (μ[g|↑ℱ n]) x) atTop (𝓝 (g x))
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>R✝ : ℝ≥0<VAR>inst✝ : IsFiniteMeasure μ<VAR>g : Ω → ℝ<VAR>hg : Integrable g μ<VAR>hgmeas : StronglyMeasurable g<VAR>hle : ⨆ n, ↑ℱ n ≤ m0<VAR>hunif : UniformIntegrable (fun n => μ[g|↑ℱ n]) 1 μ<VAR>R : ℝ≥0<VAR>hR : ∀ (i : ℕ), eLpNorm ((fun n => μ[g|↑ℱ n]) i) 1 μ ≤ ↑R<GOAL>∀ᵐ (x : Ω) ∂μ, Tendsto (fun n => (μ[g|↑ℱ n]) x) atTop (𝓝 (g x))
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>R✝ : ℝ≥0<VAR>inst✝ : IsFiniteMeasure μ<VAR>g : Ω → ℝ<VAR>hg : Integrable g μ<VAR>hgmeas : StronglyMeasurable g<VAR>hle : ⨆ n, ↑ℱ n ≤ m0<VAR>hunif : UniformIntegrable (fun n => μ[g|↑ℱ n]) 1 μ<VAR>R : ℝ≥0<VAR>hR : ∀ (i : ℕ), eLpNorm ((fun n => μ[g|↑ℱ n]) i) 1 μ ≤ ↑R<VAR>hlimint : Integrable (limitProcess (fun n => μ[g|↑ℱ n]) ℱ μ) μ<GOAL>∀ᵐ (x : Ω) ∂μ, Tendsto (fun n => (μ[g|↑ℱ n]) x) atTop (𝓝 (g x))
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>R✝ : ℝ≥0<VAR>inst✝ : IsFiniteMeasure μ<VAR>g : Ω → ℝ<VAR>hg : Integrable g μ<VAR>hgmeas : StronglyMeasurable g<VAR>hle : ⨆ n, ↑ℱ n ≤ m0<VAR>hunif : UniformIntegrable (fun n => μ[g|↑ℱ n]) 1 μ<VAR>R : ℝ≥0<VAR>hR : ∀ (i : ℕ), eLpNorm ((fun n => μ[g|↑ℱ n]) i) 1 μ ≤ ↑R<VAR>hlimint : Integrable (limitProcess (fun n => μ[g|↑ℱ n]) ℱ μ) μ<GOAL>g =ᶠ[ae μ] limitProcess (fun n x => (μ[g|↑ℱ n]) x) ℱ μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>R✝ : ℝ≥0<VAR>inst✝ : IsFiniteMeasure μ<VAR>g : Ω → ℝ<VAR>hg : Integrable g μ<VAR>hgmeas : StronglyMeasurable g<VAR>hle : ⨆ n, ↑ℱ n ≤ m0<VAR>hunif : UniformIntegrable (fun n => μ[g|↑ℱ n]) 1 μ<VAR>R : ℝ≥0<VAR>hR : ∀ (i : ℕ), eLpNorm ((fun n => μ[g|↑ℱ n]) i) 1 μ ≤ ↑R<VAR>hlimint : Integrable (limitProcess (fun n => μ[g|↑ℱ n]) ℱ μ) μ<VAR>this : ∀ (n : ℕ) (s : Set Ω), MeasurableSet s → ∫ (x : Ω) in s, g x ∂μ = ∫ (x : Ω) in s, limitProcess (fun n x => (μ[g|↑ℱ n]) x) ℱ μ x ∂μ<GOAL>g =ᶠ[ae μ] limitProcess (fun n x => (μ[g|↑ℱ n]) x) ℱ μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>R✝ : ℝ≥0<VAR>inst✝ : IsFiniteMeasure μ<VAR>g : Ω → ℝ<VAR>hg : Integrable g μ<VAR>hgmeas : StronglyMeasurable g<VAR>hle : ⨆ n, ↑ℱ n ≤ m0<VAR>hunif : UniformIntegrable (fun n => μ[g|↑ℱ n]) 1 μ<VAR>R : ℝ≥0<VAR>hR : ∀ (i : ℕ), eLpNorm ((fun n => μ[g|↑ℱ n]) i) 1 μ ≤ ↑R<VAR>hlimint : Integrable (limitProcess (fun n => μ[g|↑ℱ n]) ℱ μ) μ<VAR>this : ∀ (n : ℕ) (s : Set Ω), MeasurableSet s → ∫ (x : Ω) in s, g x ∂μ = ∫ (x : Ω) in s, limitProcess (fun n x => (μ[g|↑ℱ n]) x) ℱ μ x ∂μ<VAR>s : Set Ω<VAR>hs : MeasurableSet s<GOAL>μ s < ⊤ → ∫ (x : Ω) in s, g x ∂μ = ∫ (x : Ω) in s, limitProcess (fun n x => (μ[g|↑ℱ n]) x) ℱ μ x ∂μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>R✝ : ℝ≥0<VAR>inst✝ : IsFiniteMeasure μ<VAR>g : Ω → ℝ<VAR>hg : Integrable g μ<VAR>hgmeas : StronglyMeasurable g<VAR>hle : ⨆ n, ↑ℱ n ≤ m0<VAR>hunif : UniformIntegrable (fun n => μ[g|↑ℱ n]) 1 μ<VAR>R : ℝ≥0<VAR>hR : ∀ (i : ℕ), eLpNorm ((fun n => μ[g|↑ℱ n]) i) 1 μ ≤ ↑R<VAR>hlimint : Integrable (limitProcess (fun n => μ[g|↑ℱ n]) ℱ μ) μ<VAR>this : ∀ (n : ℕ) (s : Set Ω), MeasurableSet s → ∫ (x : Ω) in s, g x ∂μ = ∫ (x : Ω) in s, limitProcess (fun n x => (μ[g|↑ℱ n]) x) ℱ μ x ∂μ<VAR>s : Set Ω<VAR>hs : MeasurableSet s<GOAL>IsPiSystem {s | ∃ n, MeasurableSet s}
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>R✝ : ℝ≥0<VAR>inst✝ : IsFiniteMeasure μ<VAR>g : Ω → ℝ<VAR>hg : Integrable g μ<VAR>hgmeas : StronglyMeasurable g<VAR>hle : ⨆ n, ↑ℱ n ≤ m0<VAR>hunif : UniformIntegrable (fun n => μ[g|↑ℱ n]) 1 μ<VAR>R : ℝ≥0<VAR>hR : ∀ (i : ℕ), eLpNorm ((fun n => μ[g|↑ℱ n]) i) 1 μ ≤ ↑R<VAR>hlimint : Integrable (limitProcess (fun n => μ[g|↑ℱ n]) ℱ μ) μ<VAR>this : ∀ (n : ℕ) (s : Set Ω), MeasurableSet s → ∫ (x : Ω) in s, g x ∂μ = ∫ (x : Ω) in s, limitProcess (fun n x => (μ[g|↑ℱ n]) x) ℱ μ x ∂μ<VAR>s : Set Ω<VAR>hs : MeasurableSet s<GOAL>μ ∅ < ⊤ → ∫ (x : Ω) in ∅, g x ∂μ = ∫ (x : Ω) in ∅, limitProcess (fun n x => (μ[g|↑ℱ n]) x) ℱ μ x ∂μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>R✝ : ℝ≥0<VAR>inst✝ : IsFiniteMeasure μ<VAR>g : Ω → ℝ<VAR>hg : Integrable g μ<VAR>hgmeas : StronglyMeasurable g<VAR>hle : ⨆ n, ↑ℱ n ≤ m0<VAR>hunif : UniformIntegrable (fun n => μ[g|↑ℱ n]) 1 μ<VAR>R : ℝ≥0<VAR>hR : ∀ (i : ℕ), eLpNorm ((fun n => μ[g|↑ℱ n]) i) 1 μ ≤ ↑R<VAR>hlimint : Integrable (limitProcess (fun n => μ[g|↑ℱ n]) ℱ μ) μ<VAR>this : ∀ (n : ℕ) (s : Set Ω), MeasurableSet s → ∫ (x : Ω) in s, g x ∂μ = ∫ (x : Ω) in s, limitProcess (fun n x => (μ[g|↑ℱ n]) x) ℱ μ x ∂μ<VAR>s : Set Ω<VAR>hs : MeasurableSet s<GOAL>∀ t ∈ {s | ∃ n, MeasurableSet s}, μ t < ⊤ → ∫ (x : Ω) in t, g x ∂μ = ∫ (x : Ω) in t, limitProcess (fun n x => (μ[g|↑ℱ n]) x) ℱ μ x ∂μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>R✝ : ℝ≥0<VAR>inst✝ : IsFiniteMeasure μ<VAR>g : Ω → ℝ<VAR>hg : Integrable g μ<VAR>hgmeas : StronglyMeasurable g<VAR>hle : ⨆ n, ↑ℱ n ≤ m0<VAR>hunif : UniformIntegrable (fun n => μ[g|↑ℱ n]) 1 μ<VAR>R : ℝ≥0<VAR>hR : ∀ (i : ℕ), eLpNorm ((fun n => μ[g|↑ℱ n]) i) 1 μ ≤ ↑R<VAR>hlimint : Integrable (limitProcess (fun n => μ[g|↑ℱ n]) ℱ μ) μ<VAR>this : ∀ (n : ℕ) (s : Set Ω), MeasurableSet s → ∫ (x : Ω) in s, g x ∂μ = ∫ (x : Ω) in s, limitProcess (fun n x => (μ[g|↑ℱ n]) x) ℱ μ x ∂μ<VAR>s : Set Ω<VAR>hs : MeasurableSet s<GOAL>∀ (t : Set Ω), MeasurableSet t → (μ t < ⊤ → ∫ (x : Ω) in t, g x ∂μ = ∫ (x : Ω) in t, limitProcess (fun n x => (μ[g|↑ℱ n]) x) ℱ μ x ∂μ) → μ tᶜ < ⊤ → ∫ (x : Ω) in tᶜ, g x ∂μ = ∫ (x : Ω) in tᶜ, limitProcess (fun n x => (μ[g|↑ℱ n]) x) ℱ μ x ∂μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>R✝ : ℝ≥0<VAR>inst✝ : IsFiniteMeasure μ<VAR>g : Ω → ℝ<VAR>hg : Integrable g μ<VAR>hgmeas : StronglyMeasurable g<VAR>hle : ⨆ n, ↑ℱ n ≤ m0<VAR>hunif : UniformIntegrable (fun n => μ[g|↑ℱ n]) 1 μ<VAR>R : ℝ≥0<VAR>hR : ∀ (i : ℕ), eLpNorm ((fun n => μ[g|↑ℱ n]) i) 1 μ ≤ ↑R<VAR>hlimint : Integrable (limitProcess (fun n => μ[g|↑ℱ n]) ℱ μ) μ<VAR>this : ∀ (n : ℕ) (s : Set Ω), MeasurableSet s → ∫ (x : Ω) in s, g x ∂μ = ∫ (x : Ω) in s, limitProcess (fun n x => (μ[g|↑ℱ n]) x) ℱ μ x ∂μ<VAR>s : Set Ω<VAR>hs : MeasurableSet s<GOAL>∀ (f : ℕ → Set Ω), Pairwise (Disjoint on f) → (∀ (i : ℕ), MeasurableSet (f i)) → (∀ (i : ℕ), μ (f i) < ⊤ → ∫ (x : Ω) in f i, g x ∂μ = ∫ (x : Ω) in f i, limitProcess (fun n x => (μ[g|↑ℱ n]) x) ℱ μ x ∂μ) → μ (⋃ i, f i) < ⊤ → ∫ (x : Ω) in ⋃ i, f i, g x ∂μ = ∫ (x : Ω) in ⋃ i, f i, limitProcess (fun n x => (μ[g|↑ℱ n]) x) ℱ μ x ∂μ
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>K K' : ChainComplex C ℕ<VAR>f : K ⟶ K'<VAR>Δ Δ' Δ'' : SimplexCategory<VAR>n : ℕ<GOAL>Isδ₀ (SimplexCategory.δ 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>hf : IsRatCondKernelCDFAux f κ ν<VAR>a : α<GOAL>∀ᵐ (t : β) ∂ν a, ∀ (q : ℚ), BddBelow (range fun r => f (a, t) ↑r)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>hf : IsRatCondKernelCDFAux f κ ν<VAR>a : α<VAR>c : β<VAR>hc : ∀ (q : ℚ), 0 ≤ f (a, c) q<GOAL>∀ (q : ℚ), BddBelow (range fun r => f (a, c) ↑r)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>hf : IsRatCondKernelCDFAux f κ ν<VAR>a : α<VAR>c : β<VAR>hc : ∀ (q : ℚ), 0 ≤ f (a, c) q<VAR>q : ℚ<GOAL>0 ∈ lowerBounds (range fun r => f (a, c) ↑r)
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝ : Category.{v₃, u₃} E<VAR>F G : C ⥤ D<VAR>X Y : C<VAR>α : F ⟶ G<VAR>f : X ⟶ Y<VAR>x✝ : IsIso (α.app Y)<GOAL>α.app X ≫ G.map f ≫ inv (α.app Y) = F.map f
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>x : ↑(Proj.restrict ⋯).toTopCat<GOAL>(toSpec 𝒜 f).val.base x = (PrimeSpectrum.comap (mapId 𝒜 ⋯)) (closedPoint (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal))
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>x : ↑(Proj.restrict ⋯).toTopCat<GOAL>(PrimeSpectrum.comap (awayToΓ 𝒜 f ≫ (Proj.restrict ⋯).presheaf.Γgerm x)) (closedPoint ↑((Proj.restrict ⋯).presheaf.stalk x)) = (PrimeSpectrum.comap (mapId 𝒜 ⋯)) (closedPoint (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal))
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>x : ↑(Proj.restrict ⋯).toTopCat<GOAL>((PrimeSpectrum.comap (mapId 𝒜 ⋯)).comp (PrimeSpectrum.comap ((Proj.stalkIso' 𝒜 ↑x).toCommRingCatIso.inv ≫ (Proj.restrictStalkIso ⋯ x).inv))) (closedPoint ↑((Proj.restrict ⋯).presheaf.stalk x)) = (PrimeSpectrum.comap (mapId 𝒜 ⋯)) (closedPoint (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹⁹ : CommSemiring R<VAR>inst✝¹⁸ : AddCommMonoid M<VAR>inst✝¹⁷ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝¹⁶ : CommRing R₁<VAR>inst✝¹⁵ : AddCommGroup M₁<VAR>inst✝¹⁴ : Module R₁ M₁<VAR>R₂ : Type u_5<VAR>M₂ : Type u_6<VAR>inst✝¹³ : CommSemiring R₂<VAR>inst✝¹² : AddCommMonoid M₂<VAR>inst✝¹¹ : Module R₂ M₂<VAR>R₃ : Type u_7<VAR>M₃ : Type u_8<VAR>inst✝¹⁰ : CommRing R₃<VAR>inst✝⁹ : AddCommGroup M₃<VAR>inst✝⁸ : Module R₃ M₃<VAR>V : Type u_9<VAR>K : Type u_10<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : AddCommGroup V<VAR>inst✝⁵ : Module K V<VAR>B✝ : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>B₂ : BilinForm R₂ M₂<VAR>A : Type u_11<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : IsDomain A<VAR>inst✝² : Module A M₃<VAR>B₃ : BilinForm A M₃<VAR>ι : Type u_12<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>B : BilinForm A M₃<VAR>b : Basis ι A M₃<GOAL>B.Nondegenerate ↔ ((BilinForm.toMatrix b) B).det ≠ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>n : ℕ<VAR>a : α<VAR>l : Vector α n<GOAL>Tendsto (fun p => p.1 ::ᵥ p.2) (𝓝 a ×ˢ 𝓝 l) (𝓝 (a ::ᵥ l))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>n : ℕ<VAR>a : α<VAR>l : Vector α n<GOAL>Tendsto (fun x => ↑(x.1 ::ᵥ x.2)) (𝓝 a ×ˢ 𝓝 l) (𝓝 (a :: ↑l))
<VAR>Ω : Type u_1<VAR>F : Type u_2<VAR>m mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f : Ω → F<VAR>inst✝ : TopologicalSpace F<VAR>hm : m ≤ mΩ<VAR>hf : AEStronglyMeasurable f μ<GOAL>AEStronglyMeasurable (fun x => f x.2) (Measure.map (fun ω => (id ω, id ω)) μ)
<VAR>Ω : Type u_1<VAR>F : Type u_2<VAR>m mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f : Ω → F<VAR>inst✝ : TopologicalSpace F<VAR>hm : m ≤ mΩ<VAR>hf : AEStronglyMeasurable (fun x => f x.2) (Measure.map (fun ω => (id ω, ω)) μ)<GOAL>AEStronglyMeasurable (fun x => f x.2) (Measure.map (fun ω => (id ω, id ω)) μ)
<VAR>r✝ r₁ r₂ : ℝ≥0<VAR>x y : ℝ<VAR>α : Type u_1<VAR>f : α → ℝ≥0<VAR>s : Finset α<VAR>r : ℝ≥0<GOAL>s.sup f / r = s.sup fun a => f a / r
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>h : S.RightHomologyData<VAR>inst✝ : S.HasRightHomology<GOAL>rightHomologyMap' (𝟙 S) h S.rightHomologyData ≫ S.rightHomologyData.ι = h.ι ≫ opcyclesMap' (𝟙 S) h S.rightHomologyData
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>p q : MvPolynomial σ R<VAR>inst✝ : CommSemiring S<VAR>f₁ : R →+* S<VAR>g₁ g₂ : σ → S<VAR>p₁ : MvPolynomial σ R<VAR>h : ∀ i ∈ p₁.vars, i ∈ p₁.vars → g₁ i = g₂ i<GOAL>(eval₂Hom f₁ g₁) p₁ = (eval₂Hom f₁ g₂) p₁
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>p q : MvPolynomial σ R<VAR>inst✝ : CommSemiring S<VAR>f₁ : R →+* S<VAR>g₁ g₂ : σ → S<VAR>p₁ : MvPolynomial σ R<VAR>h : ∀ i ∈ p₁.vars, i ∈ p₁.vars → g₁ i = g₂ i<GOAL>(eval₂Hom f₁ g₁) (∑ v ∈ p₁.support, (monomial v) (coeff v p₁)) = (eval₂Hom f₁ g₂) (∑ v ∈ p₁.support, (monomial v) (coeff v p₁))
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>p q : MvPolynomial σ R<VAR>inst✝ : CommSemiring S<VAR>f₁ : R →+* S<VAR>g₁ g₂ : σ → S<VAR>p₁ : MvPolynomial σ R<VAR>h : ∀ i ∈ p₁.vars, i ∈ p₁.vars → g₁ i = g₂ i<GOAL>(∑ x ∈ p₁.support, f₁ (coeff x p₁) * x.prod fun i k => g₁ i ^ k) = ∑ x ∈ p₁.support, f₁ (coeff x p₁) * x.prod fun i k => g₂ i ^ k
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>p q : MvPolynomial σ R<VAR>inst✝ : CommSemiring S<VAR>f₁ : R →+* S<VAR>g₁ g₂ : σ → S<VAR>p₁ : MvPolynomial σ R<VAR>h : ∀ i ∈ p₁.vars, i ∈ p₁.vars → g₁ i = g₂ i<GOAL>∀ x ∈ p₁.support, (f₁ (coeff x p₁) * x.prod fun i k => g₁ i ^ k) = f₁ (coeff x p₁) * x.prod fun i k => g₂ i ^ k
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>p q : MvPolynomial σ R<VAR>inst✝ : CommSemiring S<VAR>f₁ : R →+* S<VAR>g₁ g₂ : σ → S<VAR>p₁ : MvPolynomial σ R<VAR>h : ∀ i ∈ p₁.vars, i ∈ p₁.vars → g₁ i = g₂ i<VAR>d : σ →₀ ℕ<VAR>hd : d ∈ p₁.support<GOAL>∏ x ∈ d.support, g₁ x ^ d x = ∏ x ∈ d.support, g₂ x ^ d x
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>p q : MvPolynomial σ R<VAR>inst✝ : CommSemiring S<VAR>f₁ : R →+* S<VAR>g₁ g₂ : σ → S<VAR>p₁ : MvPolynomial σ R<VAR>h : ∀ i ∈ p₁.vars, i ∈ p₁.vars → g₁ i = g₂ i<VAR>d : σ →₀ ℕ<VAR>hd : d ∈ p₁.support<GOAL>∀ x ∈ d.support, g₁ x ^ d x = g₂ x ^ d x
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>p q : MvPolynomial σ R<VAR>inst✝ : CommSemiring S<VAR>f₁ : R →+* S<VAR>g₁ g₂ : σ → S<VAR>p₁ : MvPolynomial σ R<VAR>h : ∀ i ∈ p₁.vars, i ∈ p₁.vars → g₁ i = g₂ i<VAR>d : σ →₀ ℕ<VAR>hd : d ∈ p₁.support<VAR>i : σ<VAR>hi : i ∈ d.support<GOAL>g₁ i ^ d i = g₂ i ^ d i
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>p q : MvPolynomial σ R<VAR>inst✝ : CommSemiring S<VAR>f₁ : R →+* S<VAR>g₁ g₂ : σ → S<VAR>p₁ : MvPolynomial σ R<VAR>h : ∀ i ∈ p₁.vars, i ∈ p₁.vars → g₁ i = g₂ i<VAR>d : σ →₀ ℕ<VAR>hd : d ∈ p₁.support<VAR>i : σ<VAR>hi : i ∈ d.support<VAR>this : i ∈ p₁.vars<GOAL>g₁ i ^ d i = g₂ i ^ d i
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : NormedAddCommGroup F'<VAR>inst✝³ : NormedSpace ℝ F'<VAR>inst✝² : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : NormedField 𝕜<VAR>inst✝ : NormedSpace 𝕜 E<VAR>T : Set α → E →L[ℝ] F<VAR>C : ℝ<VAR>hT_norm : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ‖T s‖ ≤ C * (μ s).toReal<VAR>f : ↥(simpleFunc E 1 μ)<GOAL>‖setToL1S T f‖ ≤ C * ‖f‖
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : NormedAddCommGroup F'<VAR>inst✝³ : NormedSpace ℝ F'<VAR>inst✝² : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : NormedField 𝕜<VAR>inst✝ : NormedSpace 𝕜 E<VAR>T : Set α → E →L[ℝ] F<VAR>C : ℝ<VAR>hT_norm : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ‖T s‖ ≤ C * (μ s).toReal<VAR>f : ↥(simpleFunc E 1 μ)<GOAL>‖SimpleFunc.setToSimpleFunc T (toSimpleFunc f)‖ ≤ C * ∑ x ∈ (toSimpleFunc f).range, (μ (↑(toSimpleFunc f) ⁻¹' {x})).toReal * ‖x‖
<VAR>x : ℂ<GOAL>sin (↑π / 2 - x) = cos x
<VAR>ι : Sort u_1<VAR>f g : ι → ℝ≥0∞<VAR>a✝ b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>a : ℝ≥0∞<GOAL>a + iInf f = ⨅ b, a + f b
<VAR>ι : Sort u_1<VAR>f g : ι → ℝ≥0∞<VAR>a✝ b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>a : ℝ≥0∞<GOAL>⨅ i, f i + a = ⨅ b, a + f b
<VAR>X✝ Y✝ : Scheme<VAR>f✝ : X✝ ⟶ Y✝<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>inst✝ : IsAffine Y<GOAL>QuasiSeparated f ↔ QuasiSeparatedSpace ↑↑X.toPresheafedSpace
<VAR>a b n : ℕ<GOAL>(if n = 0 ∨ a = 0 then 0 else a.factorization.prod fun p k => p ^ (k / n)) = if n = 0 ∨ a = 0 then 0 else (a.factorization ⌊/⌋ n).prod fun x x_1 => x ^ x_1
<VAR>α : Type u_1<VAR>inst✝ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>x : α<VAR>P : Set α → Prop<GOAL>(∃ᶠ (a : Set α) in v.filterAt x, P a) ↔ ∀ ε > 0, ∃ a ∈ v.setsAt x, a ⊆ closedBall x ε ∧ P a
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>l₁ l₂ : List α<GOAL>l₁ <+~ l₂ ↔ ∀ (x : α), x ∈ l₁ → count x l₁ ≤ count x l₂
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>l₁ l₂ : List α<VAR>h : ∀ (x : α), x ∈ l₁ → count x l₁ ≤ count x l₂<GOAL>l₁ <+~ l₂
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>l₁ l₂ : List α<VAR>h : ∀ (x : α), x ∈ l₁ → count x l₁ ≤ count x l₂<VAR>this : l₁ <+~ l₂.diff l₁ ++ l₁<GOAL>l₁ <+~ l₂
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>l₁ l₂ : List α<VAR>h : ∀ (x : α), x ∈ l₁ → count x l₁ ≤ count x l₂<VAR>this : l₁ <+~ l₂.diff l₁ ++ l₁<GOAL>l₂.diff l₁ ++ l₁ ~ l₂
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>P : Prop<VAR>inst✝ : LocalRing R<VAR>h_pos : ∀ (p : ℕ), IsPrimePow p → CharP R p → P<VAR>h_equal : Algebra ℚ R → P<VAR>h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P<GOAL>P