ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>ℱ : MeasureTheory.Filtration ℕ m0<VAR>s : ℕ → Set Ω<VAR>hs : ∀ (n : ℕ), MeasurableSet (s n)<GOAL>MeasureTheory.Adapted ℱ (MeasureTheory.BorelCantelli.process s)
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>ℱ : MeasureTheory.Filtration ℕ m0<VAR>μ : MeasureTheory.Measure Ω<VAR>s : ℕ → Set Ω<VAR>n : ℕ<GOAL>MeasureTheory.martingalePart (MeasureTheory.BorelCantelli.process s) ℱ μ n = ∑ k ∈ Finset.range n, ((s (k + 1)).indicator 1 - μ[(s (k + 1)).indicator 1|↑ℱ k])
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>ℱ : MeasureTheory.Filtration ℕ m0<VAR>μ : MeasureTheory.Measure Ω<VAR>s : ℕ → Set Ω<VAR>n : ℕ<GOAL>MeasureTheory.predictablePart (MeasureTheory.BorelCantelli.process s) ℱ μ n = ∑ k ∈ Finset.range n, μ[(s (k + 1)).indicator 1|↑ℱ k]
<VAR>Ω : Type u_1<VAR>s : ℕ → Set Ω<VAR>ω : Ω<VAR>n : ℕ<GOAL>|MeasureTheory.BorelCantelli.process s (n + 1) ω - MeasureTheory.BorelCantelli.process s n ω| ≤ ↑1
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>ℱ : MeasureTheory.Filtration ℕ m0<VAR>s : ℕ → Set Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hs : ∀ (n : ℕ), MeasurableSet (s n)<VAR>n : ℕ<GOAL>MeasureTheory.Integrable (MeasureTheory.BorelCantelli.process s n) μ
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>ℱ : MeasureTheory.Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>R : ℝ≥0<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hfmono : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), f n ω ≤ f (n + 1) ω<VAR>hf : MeasureTheory.Adapted ℱ f<VAR>hint : ∀ (n : ℕ), MeasureTheory.Integrable (f n) μ<VAR>hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), |f (n + 1) ω - f n ω| ≤ ↑R<GOAL>∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun n => f n ω) Filter.atTop Filter.atTop ↔ Filter.Tendsto (fun n => MeasureTheory.predictablePart f ℱ μ n ω) Filter.atTop Filter.atTop
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>ℱ : MeasureTheory.Filtration ℕ m0<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>s : ℕ → Set Ω<VAR>hs : ∀ (n : ℕ), MeasurableSet (s n)<GOAL>∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun n => ∑ k ∈ Finset.range n, (s (k + 1)).indicator 1 ω) Filter.atTop Filter.atTop ↔ Filter.Tendsto (fun n => ∑ k ∈ Finset.range n, (μ[(s (k + 1)).indicator 1|↑ℱ k]) ω) Filter.atTop Filter.atTop
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>ℱ : MeasureTheory.Filtration ℕ m0<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>s : ℕ → Set Ω<VAR>hs : ∀ (n : ℕ), MeasurableSet (s n)<GOAL>∀ᵐ (ω : Ω) ∂μ, ω ∈ Filter.limsup s Filter.atTop ↔ Filter.Tendsto (fun n => ∑ k ∈ Finset.range n, (μ[(s (k + 1)).indicator 1|↑ℱ k]) ω) Filter.atTop Filter.atTop
<VAR>R : Type u_1<VAR>CommRing R<VAR>a b : R[X]<GOAL>((Polynomial.wronskianBilin R) a) b = a.wronskian b
<VAR>R : Type u_1<VAR>CommRing R<VAR>a : R[X]<GOAL>Polynomial.wronskian 0 a = 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>a : R[X]<GOAL>a.wronskian 0 = 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>a b : R[X]<GOAL>(-a).wronskian b = -a.wronskian b
<VAR>R : Type u_1<VAR>CommRing R<VAR>a b : R[X]<GOAL>a.wronskian (-b) = -a.wronskian b
<VAR>R : Type u_1<VAR>CommRing R<VAR>a b c : R[X]<GOAL>a.wronskian (b + c) = a.wronskian b + a.wronskian c
<VAR>R : Type u_1<VAR>CommRing R<VAR>a b c : R[X]<GOAL>(a + b).wronskian c = a.wronskian c + b.wronskian c
<VAR>R : Type u_1<VAR>CommRing R<VAR>a : R[X]<GOAL>a.wronskian a = 0
<VAR>R : Type u_1<VAR>CommRing R<GOAL>(Polynomial.wronskianBilin R).IsAlt
<VAR>R : Type u_1<VAR>CommRing R<VAR>a b : R[X]<GOAL>-a.wronskian b = b.wronskian a
<VAR>R : Type u_1<VAR>CommRing R<VAR>a b c : R[X]<VAR>hAdd : a + b + c = 0<GOAL>a.wronskian b = b.wronskian c
<VAR>R : Type u_1<VAR>CommRing R<VAR>a b : R[X]<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<GOAL>(a.wronskian b).degree < a.degree + b.degree
<VAR>R : Type u_1<VAR>CommRing R<VAR>a b : R[X]<VAR>hw : a.wronskian b ≠ 0<GOAL>(a.wronskian b).natDegree < a.natDegree + b.natDegree
<VAR>R : Type u<VAR>Semiring R<GOAL>Polynomial.integralNormalization 0 = 0
<VAR>R : Type u<VAR>Semiring R<VAR>f : R[X]<VAR>i : ℕ<GOAL>f.integralNormalization.coeff i = if f.degree = ↑i then 1 else f.coeff i * f.leadingCoeff ^ (f.natDegree - 1 - i)
<VAR>R : Type u<VAR>Semiring R<VAR>f : R[X]<GOAL>f.integralNormalization.support ⊆ f.support
<VAR>R : Type u<VAR>Semiring R<VAR>f : R[X]<VAR>i : ℕ<VAR>hi : f.degree = ↑i<GOAL>f.integralNormalization.coeff i = 1
<VAR>R : Type u<VAR>Semiring R<VAR>f : R[X]<VAR>hf : f ≠ 0<GOAL>f.integralNormalization.coeff f.natDegree = 1
<VAR>R : Type u<VAR>Semiring R<VAR>f : R[X]<VAR>i : ℕ<VAR>hi : f.degree ≠ ↑i<GOAL>f.integralNormalization.coeff i = f.coeff i * f.leadingCoeff ^ (f.natDegree - 1 - i)
<VAR>R : Type u<VAR>Semiring R<VAR>f : R[X]<VAR>i : ℕ<VAR>hi : i ≠ f.natDegree<GOAL>f.integralNormalization.coeff i = f.coeff i * f.leadingCoeff ^ (f.natDegree - 1 - i)
<VAR>R : Type u<VAR>Semiring R<VAR>f : R[X]<VAR>hf : f ≠ 0<GOAL>f.integralNormalization.Monic
<VAR>R : Type u<VAR>Ring R<VAR>IsDomain R<VAR>f : R[X]<GOAL>f.integralNormalization.support = f.support
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>IsDomain R<VAR>CommSemiring S<VAR>p : R[X]<VAR>f : R →+* S<VAR>z : S<VAR>hz : Polynomial.eval₂ f z p = 0<VAR>inj : ∀ (x : R), f x = 0 → x = 0<GOAL>Polynomial.eval₂ f (z * f p.leadingCoeff) p.integralNormalization = 0
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>IsDomain R<VAR>CommSemiring S<VAR>Algebra R S<VAR>f : R[X]<VAR>z : S<VAR>hz : (Polynomial.aeval z) f = 0<VAR>inj : ∀ (x : R), (algebraMap R S) x = 0 → x = 0<GOAL>(Polynomial.aeval (z * (algebraMap R S) f.leadingCoeff)) f.integralNormalization = 0
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>Preorder ι<VAR>OrderBot ι<VAR>InfSet ι<VAR>a b : ℝ<VAR>f : ι → Ω → ℝ<VAR>N : ι<GOAL>MeasureTheory.upperCrossingTime a b f N 0 = ⊥
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>Preorder ι<VAR>OrderBot ι<VAR>InfSet ι<VAR>a b : ℝ<VAR>f : ι → Ω → ℝ<VAR>N : ι<GOAL>MeasureTheory.lowerCrossingTime a b f N 0 = MeasureTheory.hitting f (Set.Iic a) ⊥ N
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>Preorder ι<VAR>OrderBot ι<VAR>InfSet ι<VAR>a b : ℝ<VAR>f : ι → Ω → ℝ<VAR>N : ι<VAR>n : ℕ<VAR>ω : Ω<GOAL>MeasureTheory.upperCrossingTime a b f N (n + 1) ω = MeasureTheory.hitting f (Set.Ici b) (MeasureTheory.lowerCrossingTimeAux a f (MeasureTheory.upperCrossingTime a b f N n ω) N ω) N ω
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>Preorder ι<VAR>OrderBot ι<VAR>InfSet ι<VAR>a b : ℝ<VAR>f : ι → Ω → ℝ<VAR>N : ι<VAR>n : ℕ<VAR>ω : Ω<GOAL>MeasureTheory.upperCrossingTime a b f N (n + 1) ω = MeasureTheory.hitting f (Set.Ici b) (MeasureTheory.lowerCrossingTime a b f N n ω) N ω
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>ConditionallyCompleteLinearOrderBot ι<VAR>a b : ℝ<VAR>f : ι → Ω → ℝ<VAR>N : ι<VAR>n : ℕ<VAR>ω : Ω<GOAL>MeasureTheory.upperCrossingTime a b f N n ω ≤ N
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>ConditionallyCompleteLinearOrderBot ι<VAR>a b : ℝ<VAR>f : ι → Ω → ℝ<VAR>n : ℕ<VAR>ω : Ω<GOAL>MeasureTheory.upperCrossingTime a b f ⊥ n ω = ⊥
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>ConditionallyCompleteLinearOrderBot ι<VAR>a b : ℝ<VAR>f : ι → Ω → ℝ<VAR>N : ι<VAR>n : ℕ<VAR>ω : Ω<GOAL>MeasureTheory.lowerCrossingTime a b f N n ω ≤ N
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>ConditionallyCompleteLinearOrderBot ι<VAR>a b : ℝ<VAR>f : ι → Ω → ℝ<VAR>N : ι<VAR>n : ℕ<VAR>ω : Ω<GOAL>MeasureTheory.upperCrossingTime a b f N n ω ≤ MeasureTheory.lowerCrossingTime a b f N n ω
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>ConditionallyCompleteLinearOrderBot ι<VAR>a b : ℝ<VAR>f : ι → Ω → ℝ<VAR>N : ι<VAR>n : ℕ<VAR>ω : Ω<GOAL>MeasureTheory.lowerCrossingTime a b f N n ω ≤ MeasureTheory.upperCrossingTime a b f N (n + 1) ω
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>ConditionallyCompleteLinearOrderBot ι<VAR>a b : ℝ<VAR>f : ι → Ω → ℝ<VAR>N : ι<VAR>n m : ℕ<VAR>ω : Ω<VAR>hnm : n ≤ m<GOAL>MeasureTheory.lowerCrossingTime a b f N n ω ≤ MeasureTheory.lowerCrossingTime a b f N m ω
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>ConditionallyCompleteLinearOrderBot ι<VAR>a b : ℝ<VAR>f : ι → Ω → ℝ<VAR>N : ι<VAR>n m : ℕ<VAR>ω : Ω<VAR>hnm : n ≤ m<GOAL>MeasureTheory.upperCrossingTime a b f N n ω ≤ MeasureTheory.upperCrossingTime a b f N m ω
<VAR>Ω : Type u_1<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n : ℕ<VAR>ω : Ω<VAR>h : MeasureTheory.lowerCrossingTime a b f N n ω ≠ N<GOAL>MeasureTheory.stoppedValue f (MeasureTheory.lowerCrossingTime a b f N n) ω ≤ a
<VAR>Ω : Type u_1<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n : ℕ<VAR>ω : Ω<VAR>h : MeasureTheory.upperCrossingTime a b f N (n + 1) ω ≠ N<GOAL>b ≤ MeasureTheory.stoppedValue f (MeasureTheory.upperCrossingTime a b f N (n + 1)) ω
<VAR>Ω : Type u_1<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n : ℕ<VAR>ω : Ω<VAR>hab : a < b<VAR>hn : MeasureTheory.lowerCrossingTime a b f N (n + 1) ω ≠ N<GOAL>MeasureTheory.upperCrossingTime a b f N (n + 1) ω < MeasureTheory.lowerCrossingTime a b f N (n + 1) ω
<VAR>Ω : Type u_1<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n : ℕ<VAR>ω : Ω<VAR>hab : a < b<VAR>hn : MeasureTheory.upperCrossingTime a b f N (n + 1) ω ≠ N<GOAL>MeasureTheory.lowerCrossingTime a b f N n ω < MeasureTheory.upperCrossingTime a b f N (n + 1) ω
<VAR>Ω : Type u_1<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n : ℕ<VAR>ω : Ω<VAR>hab : a < b<VAR>hn : MeasureTheory.upperCrossingTime a b f N (n + 1) ω ≠ N<GOAL>MeasureTheory.upperCrossingTime a b f N n ω < MeasureTheory.upperCrossingTime a b f N (n + 1) ω
<VAR>Ω : Type u_1<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n m : ℕ<VAR>ω : Ω<VAR>hnm : n ≤ m<VAR>hn : MeasureTheory.lowerCrossingTime a b f N n ω = N<GOAL>MeasureTheory.lowerCrossingTime a b f N m ω = N
<VAR>Ω : Type u_1<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n m : ℕ<VAR>ω : Ω<VAR>hnm : n ≤ m<VAR>hn : MeasureTheory.upperCrossingTime a b f N n ω = N<GOAL>MeasureTheory.upperCrossingTime a b f N m ω = N
<VAR>Ω : Type u_1<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n m : ℕ<VAR>ω : Ω<VAR>hnm : n ≤ m<VAR>hn : N ≤ MeasureTheory.lowerCrossingTime a b f N n ω<GOAL>MeasureTheory.lowerCrossingTime a b f N m ω = N
<VAR>Ω : Type u_1<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n m : ℕ<VAR>ω : Ω<VAR>hnm : n ≤ m<VAR>hn : N ≤ MeasureTheory.upperCrossingTime a b f N n ω<GOAL>MeasureTheory.upperCrossingTime a b f N m ω = N
<VAR>Ω : Type u_1<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N : ℕ<VAR>ω : Ω<VAR>hab : a < b<GOAL>∃ n, MeasureTheory.upperCrossingTime a b f N n ω = N
<VAR>Ω : Type u_1<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N : ℕ<VAR>ω : Ω<VAR>hab : a < b<GOAL>BddAbove {n | MeasureTheory.upperCrossingTime a b f N n ω < N}
<VAR>Ω : Type u_1<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N : ℕ<VAR>ω : Ω<VAR>hN : 0 < N<GOAL>{n | MeasureTheory.upperCrossingTime a b f N n ω < N}.Nonempty
<VAR>Ω : Type u_1<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N : ℕ<VAR>ω : Ω<VAR>hab : a < b<GOAL>MeasureTheory.upperCrossingTime a b f N N ω = N
<VAR>Ω : Type u_1<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n : ℕ<VAR>ω : Ω<VAR>hab : a < b<VAR>hn : N ≤ n<GOAL>MeasureTheory.upperCrossingTime a b f N n ω = N
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n : ℕ<VAR>ℱ : MeasureTheory.Filtration ℕ m0<VAR>hf : MeasureTheory.Adapted ℱ f<GOAL>MeasureTheory.IsStoppingTime ℱ (MeasureTheory.upperCrossingTime a b f N n) ∧ MeasureTheory.IsStoppingTime ℱ (MeasureTheory.lowerCrossingTime a b f N n)
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n : ℕ<VAR>ℱ : MeasureTheory.Filtration ℕ m0<VAR>hf : MeasureTheory.Adapted ℱ f<GOAL>MeasureTheory.IsStoppingTime ℱ (MeasureTheory.upperCrossingTime a b f N n)
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n : ℕ<VAR>ℱ : MeasureTheory.Filtration ℕ m0<VAR>hf : MeasureTheory.Adapted ℱ f<GOAL>MeasureTheory.IsStoppingTime ℱ (MeasureTheory.lowerCrossingTime a b f N n)
<VAR>Ω : Type u_1<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n : ℕ<VAR>ω : Ω<GOAL>0 ≤ MeasureTheory.upcrossingStrat a b f N n ω
<VAR>Ω : Type u_1<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n : ℕ<VAR>ω : Ω<GOAL>MeasureTheory.upcrossingStrat a b f N n ω ≤ 1
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N : ℕ<VAR>ℱ : MeasureTheory.Filtration ℕ m0<VAR>hf : MeasureTheory.Adapted ℱ f<GOAL>MeasureTheory.Adapted ℱ (MeasureTheory.upcrossingStrat a b f N)
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>f : ℕ → Ω → ℝ<VAR>ℱ : MeasureTheory.Filtration ℕ m0<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hf : MeasureTheory.Submartingale f ℱ μ<VAR>a b : ℝ<VAR>N : ℕ<GOAL>MeasureTheory.Submartingale (fun n => ∑ k ∈ Finset.range n, MeasureTheory.upcrossingStrat a b f N k * (f (k + 1) - f k)) ℱ μ
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>f : ℕ → Ω → ℝ<VAR>ℱ : MeasureTheory.Filtration ℕ m0<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hf : MeasureTheory.Submartingale f ℱ μ<VAR>a b : ℝ<VAR>N : ℕ<GOAL>MeasureTheory.Submartingale (fun n => ∑ k ∈ Finset.range n, (1 - MeasureTheory.upcrossingStrat a b f N k) * (f (k + 1) - f k)) ℱ μ
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n : ℕ<VAR>ℱ : MeasureTheory.Filtration ℕ m0<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hf : MeasureTheory.Submartingale f ℱ μ<GOAL>∫ (x : Ω), (∑ k ∈ Finset.range n, MeasureTheory.upcrossingStrat a b f N k * (f (k + 1) - f k)) x ∂μ ≤ ∫ (x : Ω), f n x ∂μ - ∫ (x : Ω), f 0 x ∂μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>Preorder ι<VAR>OrderBot ι<VAR>InfSet ι<VAR>a b : ℝ<VAR>f : ι → Ω → ℝ<VAR>ω : Ω<GOAL>MeasureTheory.upcrossingsBefore a b f ⊥ ω = ⊥
<VAR>Ω : Type u_1<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<GOAL>MeasureTheory.upcrossingsBefore a b f 0 ω = 0
<VAR>Ω : Type u_1<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<GOAL>MeasureTheory.upcrossingsBefore a b f 0 = 0
<VAR>Ω : Type u_1<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n : ℕ<VAR>ω : Ω<VAR>hN : 0 < N<VAR>hab : a < b<VAR>hn : n ≤ MeasureTheory.upcrossingsBefore a b f N ω<GOAL>MeasureTheory.upperCrossingTime a b f N n ω < N
<VAR>Ω : Type u_1<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n : ℕ<VAR>ω : Ω<VAR>hab : a < b<VAR>hn : MeasureTheory.upcrossingsBefore a b f N ω < n<GOAL>MeasureTheory.upperCrossingTime a b f N n ω = N
<VAR>Ω : Type u_1<VAR>a b : ℝ<VAR>N : ℕ<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>hab : a < b<GOAL>MeasureTheory.upcrossingsBefore a b f N ω ≤ N
<VAR>Ω : Type u_1<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n : ℕ<VAR>ω : Ω<VAR>M : ℕ<VAR>hNM : N ≤ M<VAR>h : MeasureTheory.lowerCrossingTime a b f N n ω < N<GOAL>MeasureTheory.upperCrossingTime a b f M n ω = MeasureTheory.upperCrossingTime a b f N n ω ∧ MeasureTheory.lowerCrossingTime a b f M n ω = MeasureTheory.lowerCrossingTime a b f N n ω
<VAR>Ω : Type u_1<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n : ℕ<VAR>ω : Ω<VAR>M : ℕ<VAR>hNM : N ≤ M<VAR>h : MeasureTheory.upperCrossingTime a b f N (n + 1) ω < N<GOAL>MeasureTheory.upperCrossingTime a b f M (n + 1) ω = MeasureTheory.upperCrossingTime a b f N (n + 1) ω ∧ MeasureTheory.lowerCrossingTime a b f M n ω = MeasureTheory.lowerCrossingTime a b f N n ω
<VAR>Ω : Type u_1<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n : ℕ<VAR>ω : Ω<VAR>M : ℕ<VAR>hNM : N ≤ M<VAR>h : MeasureTheory.upperCrossingTime a b f N n ω < N<GOAL>MeasureTheory.upperCrossingTime a b f M n ω = MeasureTheory.upperCrossingTime a b f N n ω
<VAR>Ω : Type u_1<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>hab : a < b<GOAL>Monotone fun N ω => MeasureTheory.upcrossingsBefore a b f N ω
<VAR>Ω : Type u_1<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N : ℕ<VAR>ω : Ω<VAR>hab : a < b<VAR>N₁ N₂ : ℕ<VAR>hN₁ : N ≤ N₁<VAR>hN₁' : f N₁ ω < a<VAR>hN₂ : N₁ ≤ N₂<VAR>hN₂' : b < f N₂ ω<GOAL>MeasureTheory.upcrossingsBefore a b f N ω < MeasureTheory.upcrossingsBefore a b f (N₂ + 1) ω
<VAR>Ω : Type u_1<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n : ℕ<VAR>ω : Ω<VAR>hN : 0 < N<VAR>hab : a < b<VAR>hn : n < MeasureTheory.upcrossingsBefore a b f N ω<GOAL>MeasureTheory.lowerCrossingTime a b f N n ω < N
<VAR>Ω : Type u_1<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n : ℕ<VAR>ω : Ω<VAR>hN : 0 < N<VAR>hab : a < b<VAR>hn : n < MeasureTheory.upcrossingsBefore a b f N ω<GOAL>b - a ≤ MeasureTheory.stoppedValue f (MeasureTheory.upperCrossingTime a b f N (n + 1)) ω - MeasureTheory.stoppedValue f (MeasureTheory.lowerCrossingTime a b f N n) ω
<VAR>Ω : Type u_1<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n : ℕ<VAR>ω : Ω<VAR>hab : a < b<VAR>hn : MeasureTheory.upcrossingsBefore a b f N ω < n<GOAL>MeasureTheory.stoppedValue f (MeasureTheory.upperCrossingTime a b f N (n + 1)) ω - MeasureTheory.stoppedValue f (MeasureTheory.lowerCrossingTime a b f N n) ω = 0
<VAR>Ω : Type u_1<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N : ℕ<VAR>ω : Ω<VAR>hf : a ≤ f N ω<VAR>hab : a < b<GOAL>(b - a) * ↑(MeasureTheory.upcrossingsBefore a b f N ω) ≤ ∑ k ∈ Finset.range N, MeasureTheory.upcrossingStrat a b f N k ω * (f (k + 1) - f k) ω
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N : ℕ<VAR>ℱ : MeasureTheory.Filtration ℕ m0<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hf : MeasureTheory.Submartingale f ℱ μ<VAR>hfN : ∀ (ω : Ω), a ≤ f N ω<VAR>hfzero : 0 ≤ f 0<VAR>hab : a < b<GOAL>(b - a) * ∫ (x : Ω), ↑(MeasureTheory.upcrossingsBefore a b f N x) ∂μ ≤ ∫ (x : Ω), f N x ∂μ
<VAR>Ω : Type u_1<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n : ℕ<VAR>hab : a < b<GOAL>MeasureTheory.upperCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N n = MeasureTheory.upperCrossingTime a b f N n ∧ MeasureTheory.lowerCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N n = MeasureTheory.lowerCrossingTime a b f N n
<VAR>Ω : Type u_1<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N : ℕ<VAR>ω : Ω<VAR>hab : a < b<GOAL>MeasureTheory.upcrossingsBefore 0 (b - a) (fun n ω => (f n ω - a)⁺) N ω = MeasureTheory.upcrossingsBefore a b f N ω
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N : ℕ<VAR>ℱ : MeasureTheory.Filtration ℕ m0<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hf : MeasureTheory.Submartingale f ℱ μ<VAR>hab : a < b<GOAL>(b - a) * ∫ (x : Ω), ↑(MeasureTheory.upcrossingsBefore a b f N x) ∂μ ≤ ∫ (x : Ω), (fun ω => (f N ω - a)⁺) x ∂μ
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>f : ℕ → Ω → ℝ<VAR>ℱ : MeasureTheory.Filtration ℕ m0<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>a b : ℝ<VAR>hf : MeasureTheory.Submartingale f ℱ μ<VAR>N : ℕ<GOAL>(b - a) * ∫ (x : Ω), ↑(MeasureTheory.upcrossingsBefore a b f N x) ∂μ ≤ ∫ (x : Ω), (fun ω => (f N ω - a)⁺) x ∂μ
<VAR>Ω : Type u_1<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N : ℕ<VAR>ω : Ω<VAR>hab : a < b<GOAL>MeasureTheory.upcrossingsBefore a b f N ω = ∑ i ∈ Finset.Ico 1 (N + 1), {n | MeasureTheory.upperCrossingTime a b f N n ω < N}.indicator 1 i
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N : ℕ<VAR>ℱ : MeasureTheory.Filtration ℕ m0<VAR>hf : MeasureTheory.Adapted ℱ f<VAR>hab : a < b<GOAL>Measurable (MeasureTheory.upcrossingsBefore a b f N)
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N : ℕ<VAR>ℱ : MeasureTheory.Filtration ℕ m0<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hf : MeasureTheory.Adapted ℱ f<VAR>hab : a < b<GOAL>MeasureTheory.Integrable (fun ω => ↑(MeasureTheory.upcrossingsBefore a b f N ω)) μ
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>ℱ : MeasureTheory.Filtration ℕ m0<VAR>hf : MeasureTheory.Adapted ℱ f<VAR>hab : a < b<GOAL>Measurable (MeasureTheory.upcrossings a b f)
<VAR>Ω : Type u_1<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<GOAL>MeasureTheory.upcrossings a b f ω < ⊤ ↔ ∃ k, ∀ (N : ℕ), MeasureTheory.upcrossingsBefore a b f N ω ≤ k
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>f : ℕ → Ω → ℝ<VAR>ℱ : MeasureTheory.Filtration ℕ m0<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>a b : ℝ<VAR>hf : MeasureTheory.Submartingale f ℱ μ<GOAL>ENNReal.ofReal (b - a) * ∫⁻ (ω : Ω), MeasureTheory.upcrossings a b f ω ∂μ ≤ ⨆ N, ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ
<VAR>R : Type u<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type v<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Type w<VAR>AddCommGroup N<VAR>Module R N<VAR>f : M →ₗ[R] N<VAR>hf : Function.Surjective ⇑f<GOAL>Function.Surjective ⇑(AdicCompletion.map I f)
<VAR>R : Type u<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Type u<VAR>AddCommGroup N<VAR>Module R N<VAR>IsNoetherianRing R<VAR>Module.Finite R N<VAR>f : M →ₗ[R] N<VAR>hf : Function.Injective ⇑f<GOAL>Function.Injective ⇑(AdicCompletion.map I f)
<VAR>R : Type u<VAR>CommRing R<VAR>I : Ideal R<VAR>N : Type u<VAR>AddCommGroup N<VAR>Module R N<VAR>P : Type u<VAR>AddCommGroup P<VAR>Module R P<VAR>g : N →ₗ[R] P<VAR>hg : Function.Surjective ⇑g<VAR>k : ℕ<VAR>x : AdicCompletion.AdicCauchySequence I N<VAR>hker : ∀ (n : ℕ), g (↑x n) ∈ I ^ n • ⊤<VAR>n : ℕ<GOAL>g (↑x (k + n)) ∈ Submodule.map g (I ^ (k + n) • ⊤)
<VAR>R : Type u<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Type u<VAR>AddCommGroup N<VAR>Module R N<VAR>P : Type u<VAR>AddCommGroup P<VAR>Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>hfg : Function.Exact ⇑f ⇑g<VAR>hg : Function.Surjective ⇑g<VAR>k : ℕ<VAR>x : AdicCompletion.AdicCauchySequence I N<VAR>hker : ∀ (n : ℕ), g (↑x n) ∈ I ^ n • ⊤<VAR>n : ℕ<GOAL>∃ d y, d ∈ I ^ (k + n) • ⊤ ∧ f y = ↑x (k + n) - d
<VAR>R : Type u<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Type u<VAR>AddCommGroup N<VAR>Module R N<VAR>P : Type u<VAR>AddCommGroup P<VAR>Module R P<VAR>IsNoetherianRing R<VAR>Module.Finite R N<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>hf : Function.Injective ⇑f<VAR>hfg : Function.Exact ⇑f ⇑g<VAR>hg : Function.Surjective ⇑g<GOAL>Function.Exact ⇑(AdicCompletion.map I f) ⇑(AdicCompletion.map I g)
<VAR>m n : ℤ<GOAL>IsCoprime m n ↔ m.gcd n = 1
<VAR>m n : ℕ<GOAL>IsCoprime ↑m ↑n ↔ m.Coprime n
<VAR>R : Type u_1<VAR>CommRing R<VAR>a b : ℕ<VAR>h : a.Coprime b<GOAL>IsCoprime ↑a ↑b
<VAR>A : Type u<VAR>CommRing A<VAR>Nontrivial A<VAR>a b : ℕ<VAR>h : a.Coprime b<GOAL>↑a ≠ 0 ∨ ↑b ≠ 0
<VAR>R : Type u<VAR>I : Type v<VAR>CommSemiring R<VAR>x : R<VAR>s : I → R<VAR>t : Finset I<GOAL>(∀ i ∈ t, IsCoprime (s i) x) → IsCoprime (∏ i ∈ t, s i) x
<VAR>R : Type u<VAR>I : Type v<VAR>CommSemiring R<VAR>x : R<VAR>s : I → R<VAR>t : Finset I<GOAL>(∀ i ∈ t, IsCoprime x (s i)) → IsCoprime x (∏ i ∈ t, s i)
<VAR>R : Type u<VAR>I : Type v<VAR>CommSemiring R<VAR>x : R<VAR>s : I → R<VAR>t : Finset I<GOAL>IsCoprime (∏ i ∈ t, s i) x ↔ ∀ i ∈ t, IsCoprime (s i) x
<VAR>R : Type u<VAR>I : Type v<VAR>CommSemiring R<VAR>x : R<VAR>s : I → R<VAR>t : Finset I<GOAL>IsCoprime x (∏ i ∈ t, s i) ↔ ∀ i ∈ t, IsCoprime x (s i)
<VAR>R : Type u<VAR>I : Type v<VAR>CommSemiring R<VAR>x : R<VAR>s : I → R<VAR>t : Finset I<VAR>H1 : IsCoprime (∏ i ∈ t, s i) x<VAR>i : I<VAR>hit : i ∈ t<GOAL>IsCoprime (s i) x
<VAR>R : Type u<VAR>I : Type v<VAR>CommSemiring R<VAR>x : R<VAR>s : I → R<VAR>t : Finset I<VAR>H1 : IsCoprime x (∏ i ∈ t, s i)<VAR>i : I<VAR>hit : i ∈ t<GOAL>IsCoprime x (s i)
<VAR>R : Type u<VAR>I : Type v<VAR>CommSemiring R<VAR>z : R<VAR>s : I → R<VAR>t : Finset I<GOAL>(↑t).Pairwise (IsCoprime on s) → (∀ i ∈ t, s i ∣ z) → ∏ x ∈ t, s x ∣ z
<VAR>R : Type u<VAR>I : Type v<VAR>CommSemiring R<VAR>z : R<VAR>s : I → R<VAR>Fintype I<VAR>Hs : Pairwise (IsCoprime on s)<VAR>Hs1 : ∀ (i : I), s i ∣ z<GOAL>∏ x : I, s x ∣ z
<VAR>R : Type u<VAR>I : Type v<VAR>CommSemiring R<VAR>s : I → R<VAR>t : Finset I<VAR>DecidableEq I<VAR>h : t.Nonempty<GOAL>(∃ μ, ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i => s ↑i)
<VAR>R : Type u<VAR>I : Type v<VAR>CommSemiring R<VAR>s : I → R<VAR>Fintype I<VAR>Nonempty I<VAR>DecidableEq I<GOAL>(∃ μ, ∑ i : I, μ i * ∏ j ∈ {i}ᶜ, s j = 1) ↔ Pairwise (IsCoprime on s)
<VAR>R : Type u<VAR>I : Type v<VAR>CommSemiring R<VAR>s : I → R<VAR>t : Finset I<VAR>DecidableEq I<GOAL>Pairwise (IsCoprime on fun i => s ↑i) ↔ ∀ i ∈ t, IsCoprime (s i) (∏ j ∈ t \ {i}, s j)
<VAR>R : Type u<VAR>CommSemiring R<VAR>x y : R<VAR>m : ℕ<VAR>H : IsCoprime x y<GOAL>IsCoprime (x ^ m) y
<VAR>R : Type u<VAR>CommSemiring R<VAR>x y : R<VAR>n : ℕ<VAR>H : IsCoprime x y<GOAL>IsCoprime x (y ^ n)
<VAR>R : Type u<VAR>CommSemiring R<VAR>x y : R<VAR>m n : ℕ<VAR>H : IsCoprime x y<GOAL>IsCoprime (x ^ m) (y ^ n)
<VAR>R : Type u<VAR>CommSemiring R<VAR>x y : R<VAR>m : ℕ<VAR>hm : 0 < m<GOAL>IsCoprime (x ^ m) y ↔ IsCoprime x y
<VAR>R : Type u<VAR>CommSemiring R<VAR>x y : R<VAR>m : ℕ<VAR>hm : 0 < m<GOAL>IsCoprime x (y ^ m) ↔ IsCoprime x y
<VAR>R : Type u<VAR>CommSemiring R<VAR>x y : R<VAR>m n : ℕ<VAR>hm : 0 < m<VAR>hn : 0 < n<GOAL>IsCoprime (x ^ m) (y ^ n) ↔ IsCoprime x y