ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>inst✝¹¹ : MetricSpace α<VAR>β : Type u<VAR>inst✝¹⁰ : SecondCountableTopology α<VAR>inst✝⁹ : MeasurableSpace α<VAR>inst✝⁸ : OpensMeasurableSpace α<VAR>inst✝⁷ : HasBesicovitchCovering α<VAR>inst✝⁶ : MetricSpace β<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : BorelSpace β<VAR>inst✝³ : SecondCountableTopology β<VAR>inst✝² : HasBesicovitchCovering β<VAR>ρ μ : Measure β<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>inst✝ : IsLocallyFiniteMeasure ρ<GOAL>∀ᵐ (x : β) ∂μ, Tendsto (fun r => ρ (closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 (ρ.rnDeriv μ x))
<VAR>α : Type u_1<VAR>inst✝¹¹ : MetricSpace α<VAR>β : Type u<VAR>inst✝¹⁰ : SecondCountableTopology α<VAR>inst✝⁹ : MeasurableSpace α<VAR>inst✝⁸ : OpensMeasurableSpace α<VAR>inst✝⁷ : HasBesicovitchCovering α<VAR>inst✝⁶ : MetricSpace β<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : BorelSpace β<VAR>inst✝³ : SecondCountableTopology β<VAR>inst✝² : HasBesicovitchCovering β<VAR>ρ μ : Measure β<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>x : β<VAR>hx : Tendsto (fun a => ρ a / μ a) ((Besicovitch.vitaliFamily μ).filterAt x) (𝓝 (ρ.rnDeriv μ x))<GOAL>Tendsto (fun r => ρ (closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 (ρ.rnDeriv μ x))
<VAR>a b : Ordinal.{u_1}<VAR>a0 : 0 < a<GOAL>0 < a ^ b
<VAR>a b : Ordinal.{u_1}<VAR>a0 : 0 < a<VAR>h0 : 0 < a ^ 0<GOAL>0 < a ^ b
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>inst✝² : Field K<VAR>inst✝¹ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>inst✝ : IsCyclotomicExtension {p ^ k} ℚ K<GOAL>NumberField.discr K = (-1) ^ (φ (↑p ^ k) / 2) * ↑↑p ^ (↑p ^ (k - 1) * ((↑p - 1) * k - 1))
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>inst✝² : Field K<VAR>inst✝¹ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>inst✝ : IsCyclotomicExtension {p ^ k} ℚ K<VAR>hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ K) ↑(p ^ k)<GOAL>NumberField.discr K = (-1) ^ (φ (↑p ^ k) / 2) * ↑↑p ^ (↑p ^ (k - 1) * ((↑p - 1) * k - 1))
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>inst✝² : Field K<VAR>inst✝¹ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>inst✝ : IsCyclotomicExtension {p ^ k} ℚ K<VAR>hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ K) ↑(p ^ k)<VAR>this : NumberField K<GOAL>NumberField.discr K = (-1) ^ (φ (↑p ^ k) / 2) * ↑↑p ^ (↑p ^ (k - 1) * ((↑p - 1) * k - 1))
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>inst✝² : Field K<VAR>inst✝¹ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>inst✝ : IsCyclotomicExtension {p ^ k} ℚ K<VAR>hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ K) ↑(p ^ k)<VAR>this : NumberField K<VAR>pB₁ : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasis<GOAL>NumberField.discr K = (-1) ^ (φ (↑p ^ k) / 2) * ↑↑p ^ (↑p ^ (k - 1) * ((↑p - 1) * k - 1))
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>inst✝² : Field K<VAR>inst✝¹ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>inst✝ : IsCyclotomicExtension {p ^ k} ℚ K<VAR>hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ K) ↑(p ^ k)<VAR>this : NumberField K<VAR>pB₁ : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasis<GOAL>(algebraMap ℤ ℚ) (NumberField.discr K) = (algebraMap ℤ ℚ) ((-1) ^ (φ (↑p ^ k) / 2) * ↑↑p ^ (↑p ^ (k - 1) * ((↑p - 1) * k - 1)))
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>inst✝² : Field K<VAR>inst✝¹ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>inst✝ : IsCyclotomicExtension {p ^ k} ℚ K<VAR>hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ K) ↑(p ^ k)<VAR>this : NumberField K<VAR>pB₁ : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasis<GOAL>Algebra.discr ℚ ⇑(Basis.localizationLocalization ℚ ℤ⁰ K pB₁.basis) = (algebraMap ℤ ℚ) ((-1) ^ (φ (↑p ^ k) / 2) * ↑↑p ^ (↑p ^ (k - 1) * ((↑p - 1) * k - 1)))
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>inst✝² : Field K<VAR>inst✝¹ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>inst✝ : IsCyclotomicExtension {p ^ k} ℚ K<VAR>hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ K) ↑(p ^ k)<VAR>this : NumberField K<VAR>pB₁ : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasis<GOAL>Algebra.discr ℚ ⇑(Basis.localizationLocalization ℚ ℤ⁰ K pB₁.basis) = Algebra.discr ℚ ⇑(IsPrimitiveRoot.powerBasis ℚ hζ).basis
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>inst✝² : Field K<VAR>inst✝¹ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>inst✝ : IsCyclotomicExtension {p ^ k} ℚ K<VAR>hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ K) ↑(p ^ k)<VAR>this : NumberField K<VAR>pB₁ : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasis<GOAL>(algebraMap ℤ ℚ) ((-1) ^ (φ (↑p ^ k) / 2) * ↑↑p ^ (↑p ^ (k - 1) * ((↑p - 1) * k - 1))) = (-1) ^ (φ (↑p ^ k) / 2) * ↑↑p ^ (↑p ^ (k - 1) * ((↑p - 1) * k - 1))
<VAR>R : Type uR<VAR>M : Type uM<VAR>K : Type uK<VAR>V : Type uV<VAR>ι : Type uι<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : DecidableEq ι<VAR>b : Basis ι R M<VAR>inst✝³ : _root_.Finite ι<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>x✝ : Nonempty (V ≃ₗ[K] Dual K V)<VAR>e : V ≃ₗ[K] Dual K V<GOAL>FiniteDimensional K V
<VAR>R : Type uR<VAR>M : Type uM<VAR>K : Type uK<VAR>V : Type uV<VAR>ι : Type uι<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : DecidableEq ι<VAR>b : Basis ι R M<VAR>inst✝³ : _root_.Finite ι<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>x✝ : Nonempty (V ≃ₗ[K] Dual K V)<VAR>e : V ≃ₗ[K] Dual K V<GOAL>Module.rank K V < ℵ₀
<VAR>R : Type uR<VAR>M : Type uM<VAR>K : Type uK<VAR>V : Type uV<VAR>ι : Type uι<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : DecidableEq ι<VAR>b : Basis ι R M<VAR>inst✝³ : _root_.Finite ι<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>x✝ : Nonempty (V ≃ₗ[K] Dual K V)<VAR>e : V ≃ₗ[K] Dual K V<VAR>this : ℵ₀ ≤ Module.rank K V<GOAL>False
<VAR>R : Type uR<VAR>M : Type uM<VAR>K : Type uK<VAR>V : Type uV<VAR>ι : Type uι<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : DecidableEq ι<VAR>b : Basis ι R M<VAR>inst✝³ : _root_.Finite ι<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>x✝ : Nonempty (V ≃ₗ[K] Dual K V)<VAR>e : V ≃ₗ[K] Dual K V<VAR>this : ℵ₀ ≤ Module.rank K V<GOAL>lift.{uK, uV} (Module.rank K V) = Module.rank K (V →ₗ[K] K)
<VAR>R : Type uR<VAR>M : Type uM<VAR>K : Type uK<VAR>V : Type uV<VAR>ι : Type uι<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : DecidableEq ι<VAR>b : Basis ι R M<VAR>inst✝³ : _root_.Finite ι<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>x✝ : Nonempty (V ≃ₗ[K] Dual K V)<VAR>e : V ≃ₗ[K] Dual K V<VAR>this✝ : ℵ₀ ≤ Module.rank K V<VAR>this : lift.{max uK uV, uV} (Module.rank K V) = lift.{uV, max uK uV} (Module.rank K (Dual K V))<GOAL>lift.{uK, uV} (Module.rank K V) = Module.rank K (V →ₗ[K] K)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>a b C✝ : ℝ<VAR>f g : ℂ → E<VAR>z : ℂ<VAR>hd : DiffContOnCl ℂ f {z | 0 < z.re}<VAR>hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * Complex.abs z ^ c)<VAR>hre : SuperpolynomialDecay atTop expR fun x => ‖f ↑x‖<VAR>C : ℝ<VAR>hC : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C<GOAL>EqOn f 0 {z | 0 ≤ z.re}
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>a b C✝ : ℝ<VAR>f g : ℂ → E<VAR>z : ℂ<VAR>hd : DiffContOnCl ℂ f {z | 0 < z.re}<VAR>hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * Complex.abs z ^ c)<VAR>hre : SuperpolynomialDecay atTop expR fun x => ‖f ↑x‖<VAR>C : ℝ<VAR>hC : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C<GOAL>∀ (z : ℂ), 0 < z.re → f z = 0
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>a b C✝ : ℝ<VAR>f g✝ : ℂ → E<VAR>z : ℂ<VAR>hd : DiffContOnCl ℂ f {z | 0 < z.re}<VAR>hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * Complex.abs z ^ c)<VAR>hre : SuperpolynomialDecay atTop expR fun x => ‖f ↑x‖<VAR>C : ℝ<VAR>hC : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C<VAR>g : ℕ → ℂ → E := fun n z => cexp z ^ n • f z<GOAL>∀ (z : ℂ), 0 < z.re → f z = 0
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>a b C✝ : ℝ<VAR>f g✝ : ℂ → E<VAR>z : ℂ<VAR>hd : DiffContOnCl ℂ f {z | 0 < z.re}<VAR>hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * Complex.abs z ^ c)<VAR>hre : SuperpolynomialDecay atTop expR fun x => ‖f ↑x‖<VAR>C : ℝ<VAR>hC : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C<VAR>g : ℕ → ℂ → E := fun n z => cexp z ^ n • f z<VAR>hg : ∀ (n : ℕ) (z : ℂ), ‖g n z‖ = expR z.re ^ n * ‖f z‖<GOAL>∀ (z : ℂ), 0 < z.re → f z = 0
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>a b C✝ : ℝ<VAR>f g✝ : ℂ → E<VAR>z✝ : ℂ<VAR>hd : DiffContOnCl ℂ f {z | 0 < z.re}<VAR>hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * Complex.abs z ^ c)<VAR>hre : SuperpolynomialDecay atTop expR fun x => ‖f ↑x‖<VAR>C : ℝ<VAR>hC : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C<VAR>g : ℕ → ℂ → E := fun n z => cexp z ^ n • f z<VAR>hg : ∀ (n : ℕ) (z : ℂ), ‖g n z‖ = expR z.re ^ n * ‖f z‖<VAR>z : ℂ<VAR>hz : 0 < z.re<GOAL>f z = 0
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>a b C✝ : ℝ<VAR>f g✝ : ℂ → E<VAR>z✝ : ℂ<VAR>hd : DiffContOnCl ℂ f {z | 0 < z.re}<VAR>hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * Complex.abs z ^ c)<VAR>hre : SuperpolynomialDecay atTop expR fun x => ‖f ↑x‖<VAR>C : ℝ<VAR>hC : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C<VAR>g : ℕ → ℂ → E := fun n z => cexp z ^ n • f z<VAR>hg : ∀ (n : ℕ) (z : ℂ), ‖g n z‖ = expR z.re ^ n * ‖f z‖<VAR>z : ℂ<VAR>hz : 0 < z.re<GOAL>∀ (n : ℕ), ‖g n z‖ ≤ C
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>a b C✝ : ℝ<VAR>f g✝ : ℂ → E<VAR>z✝ : ℂ<VAR>hd : DiffContOnCl ℂ f {z | 0 < z.re}<VAR>hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * Complex.abs z ^ c)<VAR>hre : SuperpolynomialDecay atTop expR fun x => ‖f ↑x‖<VAR>C : ℝ<VAR>hC : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C<VAR>g : ℕ → ℂ → E := fun n z => cexp z ^ n • f z<VAR>hg : ∀ (n : ℕ) (z : ℂ), ‖g n z‖ = expR z.re ^ n * ‖f z‖<VAR>z : ℂ<VAR>hz : 0 < z.re<VAR>n : ℕ<GOAL>‖g n z‖ ≤ C
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>a b C✝ : ℝ<VAR>f g✝ : ℂ → E<VAR>z✝ : ℂ<VAR>hd : DiffContOnCl ℂ f {z | 0 < z.re}<VAR>hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * Complex.abs z ^ c)<VAR>hre : SuperpolynomialDecay atTop expR fun x => ‖f ↑x‖<VAR>C : ℝ<VAR>hC : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C<VAR>g : ℕ → ℂ → E := fun n z => cexp z ^ n • f z<VAR>hg : ∀ (n : ℕ) (z : ℂ), ‖g n z‖ = expR z.re ^ n * ‖f z‖<VAR>z : ℂ<VAR>hz : 0 < z.re<VAR>n : ℕ<GOAL>∃ c < 2, ∃ B, g n =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * Complex.abs z ^ c)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>a b C✝ : ℝ<VAR>f g✝ : ℂ → E<VAR>z✝ : ℂ<VAR>hd : DiffContOnCl ℂ f {z | 0 < z.re}<VAR>hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * Complex.abs z ^ c)<VAR>hre : SuperpolynomialDecay atTop expR fun x => ‖f ↑x‖<VAR>C : ℝ<VAR>hC : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C<VAR>g : ℕ → ℂ → E := fun n z => cexp z ^ n • f z<VAR>hg : ∀ (n : ℕ) (z : ℂ), ‖g n z‖ = expR z.re ^ n * ‖f z‖<VAR>z : ℂ<VAR>hz : 0 < z.re<VAR>n : ℕ<GOAL>Tendsto (fun x => g n ↑x) atTop (𝓝 0)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>a b C✝ : ℝ<VAR>f g✝ : ℂ → E<VAR>z✝ : ℂ<VAR>hd : DiffContOnCl ℂ f {z | 0 < z.re}<VAR>hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * Complex.abs z ^ c)<VAR>hre : SuperpolynomialDecay atTop expR fun x => ‖f ↑x‖<VAR>C : ℝ<VAR>hC : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C<VAR>g : ℕ → ℂ → E := fun n z => cexp z ^ n • f z<VAR>hg : ∀ (n : ℕ) (z : ℂ), ‖g n z‖ = expR z.re ^ n * ‖f z‖<VAR>z : ℂ<VAR>hz : 0 < z.re<VAR>n : ℕ<VAR>y : ℝ<GOAL>‖g n (↑y * I)‖ ≤ C
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>A : Set γ<GOAL>Tendsto (fun i => ∫ (x : γ) in A, κ.densityProcess ν i a x s ∂ν a) atTop (𝓝 (∫ (x : γ) in A, κ.density ν a x s ∂ν a))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>A : Set γ<GOAL>Tendsto (fun i => eLpNorm ((fun i x => κ.densityProcess ν i a x s) i - fun x => κ.density ν a x s) 1 (ν a)) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>A : Set γ<VAR>n : ℕ<GOAL>eLpNorm ((fun x => κ.densityProcess ν n a x s) - Filtration.limitProcess (fun n x => κ.densityProcess ν n a x s) (countableFiltration γ) (ν a)) 1 (ν a) = eLpNorm ((fun i x => κ.densityProcess ν i a x s) n - fun x => κ.density ν a x s) 1 (ν a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>A : Set γ<VAR>n : ℕ<GOAL>(fun x => κ.densityProcess ν n a x s) - Filtration.limitProcess (fun n x => κ.densityProcess ν n a x s) (countableFiltration γ) (ν a) =ᶠ[ae (ν a)] (fun i x => κ.densityProcess ν i a x s) n - fun x => κ.density ν a x s
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{?u.12795, u_1} C<VAR>inst✝⁴ : Category.{?u.12799, u_2} D<VAR>inst✝³ : HasZeroMorphisms C<VAR>inst✝² : HasZeroMorphisms D<VAR>S S₁ S₂ : ShortComplex C<VAR>h : S.LeftHomologyData<VAR>F : C ⥤ D<VAR>inst✝¹ : F.PreservesZeroMorphisms<VAR>inst✝ : h.IsPreservedBy F<VAR>this✝ : PreservesLimit (parallelPair S.g 0) F<VAR>this : PreservesColimit (parallelPair h.f' 0) F<GOAL>(S.map F).LeftHomologyData
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{?u.12795, u_1} C<VAR>inst✝⁴ : Category.{?u.12799, u_2} D<VAR>inst✝³ : HasZeroMorphisms C<VAR>inst✝² : HasZeroMorphisms D<VAR>S S₁ S₂ : ShortComplex C<VAR>h : S.LeftHomologyData<VAR>F : C ⥤ D<VAR>inst✝¹ : F.PreservesZeroMorphisms<VAR>inst✝ : h.IsPreservedBy F<VAR>this✝ : PreservesLimit (parallelPair S.g 0) F<VAR>this : PreservesColimit (parallelPair h.f' 0) F<VAR>wi : F.map h.i ≫ F.map S.g = 0<GOAL>(S.map F).LeftHomologyData
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{?u.12795, u_1} C<VAR>inst✝⁴ : Category.{?u.12799, u_2} D<VAR>inst✝³ : HasZeroMorphisms C<VAR>inst✝² : HasZeroMorphisms D<VAR>S S₁ S₂ : ShortComplex C<VAR>h : S.LeftHomologyData<VAR>F : C ⥤ D<VAR>inst✝¹ : F.PreservesZeroMorphisms<VAR>inst✝ : h.IsPreservedBy F<VAR>this✝ : PreservesLimit (parallelPair S.g 0) F<VAR>this : PreservesColimit (parallelPair h.f' 0) F<VAR>wi : F.map h.i ≫ F.map S.g = 0<VAR>hi : IsLimit ((KernelFork.ofι h.i ⋯).map F)<GOAL>(S.map F).LeftHomologyData
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{?u.12795, u_1} C<VAR>inst✝⁴ : Category.{?u.12799, u_2} D<VAR>inst✝³ : HasZeroMorphisms C<VAR>inst✝² : HasZeroMorphisms D<VAR>S S₁ S₂ : ShortComplex C<VAR>h : S.LeftHomologyData<VAR>F : C ⥤ D<VAR>inst✝¹ : F.PreservesZeroMorphisms<VAR>inst✝ : h.IsPreservedBy F<VAR>this✝ : PreservesLimit (parallelPair S.g 0) F<VAR>this : PreservesColimit (parallelPair h.f' 0) F<VAR>wi : F.map h.i ≫ F.map S.g = 0<VAR>hi : IsLimit ((KernelFork.ofι h.i ⋯).map F)<VAR>f' : F.obj S.X₁ ⟶ F.obj h.K := hi.lift (KernelFork.ofι (S.map F).f ⋯)<GOAL>(S.map F).LeftHomologyData
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{?u.12795, u_1} C<VAR>inst✝⁴ : Category.{?u.12799, u_2} D<VAR>inst✝³ : HasZeroMorphisms C<VAR>inst✝² : HasZeroMorphisms D<VAR>S S₁ S₂ : ShortComplex C<VAR>h : S.LeftHomologyData<VAR>F : C ⥤ D<VAR>inst✝¹ : F.PreservesZeroMorphisms<VAR>inst✝ : h.IsPreservedBy F<VAR>this✝ : PreservesLimit (parallelPair S.g 0) F<VAR>this : PreservesColimit (parallelPair h.f' 0) F<VAR>wi : F.map h.i ≫ F.map S.g = 0<VAR>hi : IsLimit ((KernelFork.ofι h.i ⋯).map F)<VAR>f' : F.obj S.X₁ ⟶ F.obj h.K := hi.lift (KernelFork.ofι (S.map F).f ⋯)<VAR>hf' : f' = F.map h.f'<GOAL>(S.map F).LeftHomologyData
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{?u.12795, u_1} C<VAR>inst✝⁴ : Category.{?u.12799, u_2} D<VAR>inst✝³ : HasZeroMorphisms C<VAR>inst✝² : HasZeroMorphisms D<VAR>S S₁ S₂ : ShortComplex C<VAR>h : S.LeftHomologyData<VAR>F : C ⥤ D<VAR>inst✝¹ : F.PreservesZeroMorphisms<VAR>inst✝ : h.IsPreservedBy F<VAR>this✝ : PreservesLimit (parallelPair S.g 0) F<VAR>this : PreservesColimit (parallelPair h.f' 0) F<VAR>wi : F.map h.i ≫ F.map S.g = 0<VAR>hi : IsLimit ((KernelFork.ofι h.i ⋯).map F)<VAR>f' : F.obj S.X₁ ⟶ F.obj h.K := hi.lift (KernelFork.ofι (S.map F).f ⋯)<VAR>hf' : f' = F.map h.f'<VAR>wπ : f' ≫ F.map h.π = 0<GOAL>(S.map F).LeftHomologyData
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : PartialOrder β<VAR>f : α → β<VAR>𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)<VAR>s✝ t✝ u : Finset α<VAR>a b : α<VAR>inst✝ : DecidableEq α<VAR>s t : Colex α<GOAL>s ≤ t ↔ ↑s.ofColex \ ↑t.ofColex ⊆ ↑(lowerClosure (↑t.ofColex \ ↑s.ofColex))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : CompleteLattice α<VAR>f g : Filter β<VAR>p q : β → Prop<VAR>u v : β → α<GOAL>∀ (x : β), p x → p x ∨ q x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : CompleteLattice α<VAR>f g : Filter β<VAR>p q : β → Prop<VAR>u v : β → α<GOAL>∀ (x : β), q x → p x ∨ q x
<VAR>G : Type u<VAR>inst✝² : Group G<VAR>N : Subgroup G<VAR>nN : N.Normal<VAR>H : Type v<VAR>inst✝¹ : Group H<VAR>M : Type x<VAR>inst✝ : Monoid M<VAR>x y : G<GOAL>x⁻¹ * y ∈ N ↔ ∃ z ∈ N, x * z = y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l l₁ l₂ l₃ : List α<VAR>a b : α<VAR>m n : ℕ<VAR>x y : List α<VAR>h : x <+: y<VAR>hx : x ≠ []<GOAL>x.head hx = y.head ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l l₁ l₂ l₃ : List α<VAR>a b : α<VAR>m n : ℕ<VAR>head✝ : α<VAR>tail✝ : List α<VAR>hx✝ : head✝ :: tail✝ ≠ []<VAR>h : head✝ :: tail✝ <+: []<VAR>hx : ¬False<GOAL>head✝ = [].head ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l l₁ l₂ l₃ : List α<VAR>a b : α<VAR>m n : ℕ<VAR>head✝¹ : α<VAR>tail✝¹ : List α<VAR>head✝ : α<VAR>tail✝ : List α<VAR>h : head✝¹ :: tail✝¹ <+: head✝ :: tail✝<VAR>hx : ¬False<GOAL>head✝¹ = head✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>ι : Type u_5<VAR>l : Filter ι<VAR>inst✝ : l.IsCountablyGenerated<VAR>F : ι → α → ℝ≥0∞<VAR>f bound : α → ℝ≥0∞<VAR>hF_meas : ∀ᶠ (n : ι) in l, Measurable (F n)<VAR>h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a<VAR>h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ⊤<VAR>h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))<GOAL>Tendsto (fun n => ∫⁻ (a : α), F n a ∂μ) l (𝓝 (∫⁻ (a : α), f a ∂μ))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>ι : Type u_5<VAR>l : Filter ι<VAR>inst✝ : l.IsCountablyGenerated<VAR>F : ι → α → ℝ≥0∞<VAR>f bound : α → ℝ≥0∞<VAR>hF_meas : ∀ᶠ (n : ι) in l, Measurable (F n)<VAR>h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a<VAR>h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ⊤<VAR>h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))<GOAL>∀ (x : ℕ → ι), Tendsto x atTop l → Tendsto ((fun n => ∫⁻ (a : α), F n a ∂μ) ∘ x) atTop (𝓝 (∫⁻ (a : α), f a ∂μ))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>ι : Type u_5<VAR>l : Filter ι<VAR>inst✝ : l.IsCountablyGenerated<VAR>F : ι → α → ℝ≥0∞<VAR>f bound : α → ℝ≥0∞<VAR>hF_meas : ∀ᶠ (n : ι) in l, Measurable (F n)<VAR>h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a<VAR>h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ⊤<VAR>h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))<VAR>x : ℕ → ι<VAR>xl : Tendsto x atTop l<GOAL>Tendsto ((fun n => ∫⁻ (a : α), F n a ∂μ) ∘ x) atTop (𝓝 (∫⁻ (a : α), f a ∂μ))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>ι : Type u_5<VAR>l : Filter ι<VAR>inst✝ : l.IsCountablyGenerated<VAR>F : ι → α → ℝ≥0∞<VAR>f bound : α → ℝ≥0∞<VAR>hF_meas : ∀ᶠ (n : ι) in l, Measurable (F n)<VAR>h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a<VAR>h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ⊤<VAR>h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))<VAR>x : ℕ → ι<VAR>xl : Tendsto x atTop l<VAR>hxl : ∀ s ∈ l, ∃ a, ∀ b ≥ a, x b ∈ s<GOAL>Tendsto ((fun n => ∫⁻ (a : α), F n a ∂μ) ∘ x) atTop (𝓝 (∫⁻ (a : α), f a ∂μ))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>ι : Type u_5<VAR>l : Filter ι<VAR>inst✝ : l.IsCountablyGenerated<VAR>F : ι → α → ℝ≥0∞<VAR>f bound : α → ℝ≥0∞<VAR>hF_meas : ∀ᶠ (n : ι) in l, Measurable (F n)<VAR>h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a<VAR>h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ⊤<VAR>h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))<VAR>x : ℕ → ι<VAR>xl : Tendsto x atTop l<VAR>hxl : ∀ s ∈ l, ∃ a, ∀ b ≥ a, x b ∈ s<VAR>h : {x | (fun n => Measurable (F n)) x} ∩ {x | (fun n => ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) x} ∈ l<GOAL>Tendsto ((fun n => ∫⁻ (a : α), F n a ∂μ) ∘ x) atTop (𝓝 (∫⁻ (a : α), f a ∂μ))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>ι : Type u_5<VAR>l : Filter ι<VAR>inst✝ : l.IsCountablyGenerated<VAR>F : ι → α → ℝ≥0∞<VAR>f bound : α → ℝ≥0∞<VAR>hF_meas : ∀ᶠ (n : ι) in l, Measurable (F n)<VAR>h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a<VAR>h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ⊤<VAR>h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))<VAR>x : ℕ → ι<VAR>xl : Tendsto x atTop l<VAR>hxl : ∀ s ∈ l, ∃ a, ∀ b ≥ a, x b ∈ s<VAR>k : ℕ<VAR>h : ∀ b ≥ k, x b ∈ {x | (fun n => Measurable (F n)) x} ∩ {x | (fun n => ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) x}<GOAL>Tendsto ((fun n => ∫⁻ (a : α), F n a ∂μ) ∘ x) atTop (𝓝 (∫⁻ (a : α), f a ∂μ))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>ι : Type u_5<VAR>l : Filter ι<VAR>inst✝ : l.IsCountablyGenerated<VAR>F : ι → α → ℝ≥0∞<VAR>f bound : α → ℝ≥0∞<VAR>hF_meas : ∀ᶠ (n : ι) in l, Measurable (F n)<VAR>h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a<VAR>h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ⊤<VAR>h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))<VAR>x : ℕ → ι<VAR>xl : Tendsto x atTop l<VAR>hxl : ∀ s ∈ l, ∃ a, ∀ b ≥ a, x b ∈ s<VAR>k : ℕ<VAR>h : ∀ b ≥ k, x b ∈ {x | (fun n => Measurable (F n)) x} ∩ {x | (fun n => ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) x}<GOAL>Tendsto (fun n => ((fun n => ∫⁻ (a : α), F n a ∂μ) ∘ x) (n + k)) atTop (𝓝 (∫⁻ (a : α), f a ∂μ))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>ι : Type u_5<VAR>l : Filter ι<VAR>inst✝ : l.IsCountablyGenerated<VAR>F : ι → α → ℝ≥0∞<VAR>f bound : α → ℝ≥0∞<VAR>hF_meas : ∀ᶠ (n : ι) in l, Measurable (F n)<VAR>h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a<VAR>h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ⊤<VAR>h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))<VAR>x : ℕ → ι<VAR>xl : Tendsto x atTop l<VAR>hxl : ∀ s ∈ l, ∃ a, ∀ b ≥ a, x b ∈ s<VAR>k : ℕ<VAR>h : ∀ b ≥ k, x b ∈ {x | (fun n => Measurable (F n)) x} ∩ {x | (fun n => ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) x}<GOAL>α → ℝ≥0∞
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>ι : Type u_5<VAR>l : Filter ι<VAR>inst✝ : l.IsCountablyGenerated<VAR>F : ι → α → ℝ≥0∞<VAR>f bound : α → ℝ≥0∞<VAR>hF_meas : ∀ᶠ (n : ι) in l, Measurable (F n)<VAR>h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a<VAR>h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ⊤<VAR>h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))<VAR>x : ℕ → ι<VAR>xl : Tendsto x atTop l<VAR>hxl : ∀ s ∈ l, ∃ a, ∀ b ≥ a, x b ∈ s<VAR>k : ℕ<VAR>h : ∀ b ≥ k, x b ∈ {x | (fun n => Measurable (F n)) x} ∩ {x | (fun n => ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) x}<GOAL>∀ (n : ℕ), Measurable (F (x (n + k)))