ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>MeasurableSpace.CountablyGenerated γ<VAR>κ : ProbabilityTheory.Kernel α (γ × β)<VAR>ν : ProbabilityTheory.Kernel α γ<VAR>ProbabilityTheory.IsFiniteKernel κ<VAR>n : ℕ<VAR>a : α<VAR>x : γ<VAR>seq : ℕ → Set β<VAR>hseq : Antitone seq<VAR>hseq_iInter : ⋂ i, seq i = ∅<VAR>hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)<GOAL>Filter.Tendsto (fun m => κ.densityProcess ν n a x (seq m)) Filter.atTop (𝓝 (κ.densityProcess ν n a x ∅))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>MeasurableSpace.CountablyGenerated γ<VAR>κ : ProbabilityTheory.Kernel α (γ × β)<VAR>ν : ProbabilityTheory.Kernel α γ<VAR>ProbabilityTheory.IsFiniteKernel κ<VAR>n : ℕ<VAR>a : α<VAR>x : γ<VAR>seq : ℕ → Set β<VAR>hseq : Antitone seq<VAR>hseq_iInter : ⋂ i, seq i = ∅<VAR>hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)<GOAL>Filter.Tendsto (fun m => κ.densityProcess ν n a x (seq m)) Filter.atTop (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>MeasurableSpace.CountablyGenerated γ<VAR>κ : ProbabilityTheory.Kernel α (γ × β)<VAR>ν : ProbabilityTheory.Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>ProbabilityTheory.IsFiniteKernel ν<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>∀ᵐ (x : γ) ∂ν a, Filter.Tendsto (fun n => κ.densityProcess ν n a x s) Filter.atTop (𝓝 (MeasureTheory.Filtration.limitProcess (fun n x => κ.densityProcess ν n a x s) (ProbabilityTheory.countableFiltration γ) (ν a) x))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>MeasurableSpace.CountablyGenerated γ<VAR>κ : ProbabilityTheory.Kernel α (γ × β)<VAR>ν : ProbabilityTheory.Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>ProbabilityTheory.IsFiniteKernel ν<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>MeasureTheory.Memℒp (MeasureTheory.Filtration.limitProcess (fun n x => κ.densityProcess ν n a x s) (ProbabilityTheory.countableFiltration γ) (ν a)) 1 (ν a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>MeasurableSpace.CountablyGenerated γ<VAR>κ : ProbabilityTheory.Kernel α (γ × β)<VAR>ν : ProbabilityTheory.Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>ProbabilityTheory.IsFiniteKernel ν<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>Filter.Tendsto (fun n => MeasureTheory.eLpNorm ((fun x => κ.densityProcess ν n a x s) - MeasureTheory.Filtration.limitProcess (fun n x => κ.densityProcess ν n a x s) (ProbabilityTheory.countableFiltration γ) (ν a)) 1 (ν a)) Filter.atTop (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>MeasurableSpace.CountablyGenerated γ<VAR>κ : ProbabilityTheory.Kernel α (γ × β)<VAR>ν : ProbabilityTheory.Kernel α γ<VAR>ProbabilityTheory.IsFiniteKernel ν<VAR>hκν : κ.fst ≤ ν<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>A : Set γ<GOAL>Filter.Tendsto (fun n => MeasureTheory.eLpNorm ((fun x => κ.densityProcess ν n a x s) - MeasureTheory.Filtration.limitProcess (fun n x => κ.densityProcess ν n a x s) (ProbabilityTheory.countableFiltration γ) (ν a)) 1 ((ν a).restrict A)) Filter.atTop (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>MeasurableSpace.CountablyGenerated γ<VAR>κ : ProbabilityTheory.Kernel α (γ × β)<VAR>ν : ProbabilityTheory.Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>ProbabilityTheory.IsFiniteKernel ν<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>(fun x => κ.density ν a x s) =ᵐ[ν a] MeasureTheory.Filtration.limitProcess (fun n x => κ.densityProcess ν n a x s) (ProbabilityTheory.countableFiltration γ) (ν a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>MeasurableSpace.CountablyGenerated γ<VAR>κ : ProbabilityTheory.Kernel α (γ × β)<VAR>ν : ProbabilityTheory.Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>a : α<VAR>ProbabilityTheory.IsFiniteKernel ν<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>∀ᵐ (x : γ) ∂ν a, Filter.Tendsto (fun n => κ.densityProcess ν n a x s) Filter.atTop (𝓝 (κ.density ν a x s))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>MeasurableSpace.CountablyGenerated γ<VAR>κ : ProbabilityTheory.Kernel α (γ × β)<VAR>ν : ProbabilityTheory.Kernel α γ<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>Measurable fun p => κ.density ν p.1 p.2 s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>MeasurableSpace.CountablyGenerated γ<VAR>κ : ProbabilityTheory.Kernel α (γ × β)<VAR>ν : ProbabilityTheory.Kernel α γ<VAR>x : γ<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>Measurable fun a => κ.density ν a x s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>MeasurableSpace.CountablyGenerated γ<VAR>κ : ProbabilityTheory.Kernel α (γ × β)<VAR>ν : ProbabilityTheory.Kernel α γ<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>a : α<GOAL>Measurable fun x => κ.density ν a x s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>MeasurableSpace.CountablyGenerated γ<VAR>κ : ProbabilityTheory.Kernel α (γ × β)<VAR>ν : ProbabilityTheory.Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>a : α<VAR>x : γ<VAR>s s' : Set β<VAR>h : s ⊆ s'<GOAL>κ.density ν a x s ≤ κ.density ν a x s'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>MeasurableSpace.CountablyGenerated γ<VAR>κ : ProbabilityTheory.Kernel α (γ × β)<VAR>ν : ProbabilityTheory.Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>a : α<VAR>x : γ<VAR>s : Set β<GOAL>0 ≤ κ.density ν a x s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>MeasurableSpace.CountablyGenerated γ<VAR>κ : ProbabilityTheory.Kernel α (γ × β)<VAR>ν : ProbabilityTheory.Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>a : α<VAR>x : γ<VAR>s : Set β<GOAL>κ.density ν a x s ≤ 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>MeasurableSpace.CountablyGenerated γ<VAR>κ : ProbabilityTheory.Kernel α (γ × β)<VAR>ν : ProbabilityTheory.Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>a : α<VAR>s : Set β<GOAL>MeasureTheory.eLpNorm (fun x => κ.density ν a x s) 1 (ν a) ≤ (ν a) Set.univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>MeasurableSpace.CountablyGenerated γ<VAR>κ : ProbabilityTheory.Kernel α (γ × β)<VAR>ν : ProbabilityTheory.Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>ProbabilityTheory.IsFiniteKernel ν<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>MeasureTheory.Integrable (fun x => κ.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>MeasurableSpace.CountablyGenerated γ<VAR>κ : ProbabilityTheory.Kernel α (γ × β)<VAR>ν : ProbabilityTheory.Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>ProbabilityTheory.IsFiniteKernel ν<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>A : Set γ<GOAL>Filter.Tendsto (fun i => ∫ (x : γ) in A, κ.densityProcess ν i a x s ∂ν a) Filter.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>MeasurableSpace.CountablyGenerated γ<VAR>κ : ProbabilityTheory.Kernel α (γ × β)<VAR>ν : ProbabilityTheory.Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>ProbabilityTheory.IsFiniteKernel ν<VAR>n : ℕ<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>A : Set γ<VAR>hA : MeasurableSet A<GOAL>∫ (x : γ) in A, κ.density ν a x s ∂ν a = ((κ a) (A ×ˢ s)).toReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>MeasurableSpace.CountablyGenerated γ<VAR>κ : ProbabilityTheory.Kernel α (γ × β)<VAR>ν : ProbabilityTheory.Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>ProbabilityTheory.IsFiniteKernel ν<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>∫ (x : γ), κ.density ν a x s ∂ν a = ((κ a) (Set.univ ×ˢ s)).toReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>MeasurableSpace.CountablyGenerated γ<VAR>κ : ProbabilityTheory.Kernel α (γ × β)<VAR>ν : ProbabilityTheory.Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>ProbabilityTheory.IsFiniteKernel ν<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>A : Set γ<VAR>hA : MeasurableSet A<GOAL>∫ (x : γ) in A, κ.density ν a x s ∂ν a = ((κ a) (A ×ˢ s)).toReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>MeasurableSpace.CountablyGenerated γ<VAR>κ : ProbabilityTheory.Kernel α (γ × β)<VAR>ν : ProbabilityTheory.Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>ProbabilityTheory.IsFiniteKernel ν<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>A : Set γ<VAR>hA : MeasurableSet A<GOAL>∫⁻ (x : γ) in A, ENNReal.ofReal (κ.density ν a x s) ∂ν a = (κ a) (A ×ˢ s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>MeasurableSpace.CountablyGenerated γ<VAR>κ : ProbabilityTheory.Kernel α (γ × β)<VAR>ν : ProbabilityTheory.Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>ProbabilityTheory.IsFiniteKernel ν<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>∫⁻ (x : γ), ENNReal.ofReal (κ.density ν a x s) ∂ν a = (κ a) (Set.univ ×ˢ s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>MeasurableSpace.CountablyGenerated γ<VAR>κ : ProbabilityTheory.Kernel α (γ × β)<VAR>ν : ProbabilityTheory.Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>ProbabilityTheory.IsFiniteKernel ν<VAR>a : α<VAR>seq : ℕ → Set β<VAR>hseq : Monotone seq<VAR>hseq_iUnion : ⋃ i, seq i = Set.univ<VAR>hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)<GOAL>Filter.Tendsto (fun m => ∫ (x : γ), κ.density ν a x (seq m) ∂ν a) Filter.atTop (𝓝 ((κ a) Set.univ).toReal)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>MeasurableSpace.CountablyGenerated γ<VAR>κ : ProbabilityTheory.Kernel α (γ × β)<VAR>ν : ProbabilityTheory.Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>ProbabilityTheory.IsFiniteKernel ν<VAR>a : α<VAR>seq : ℕ → Set β<VAR>hseq : Antitone seq<VAR>hseq_iInter : ⋂ i, seq i = ∅<VAR>hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)<GOAL>Filter.Tendsto (fun m => ∫ (x : γ), κ.density ν a x (seq m) ∂ν a) Filter.atTop (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>MeasurableSpace.CountablyGenerated γ<VAR>κ : ProbabilityTheory.Kernel α (γ × β)<VAR>ν : ProbabilityTheory.Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>ProbabilityTheory.IsFiniteKernel ν<VAR>a : α<VAR>seq : ℕ → Set β<VAR>hseq : Antitone seq<VAR>hseq_iInter : ⋂ i, seq i = ∅<VAR>hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)<GOAL>∀ᵐ (x : γ) ∂ν a, Filter.Tendsto (fun m => κ.density ν a x (seq m)) Filter.atTop (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>MeasurableSpace.CountablyGenerated γ<VAR>κ : ProbabilityTheory.Kernel α (γ × β)<VAR>ProbabilityTheory.IsFiniteKernel κ<VAR>n : ℕ<VAR>a : α<VAR>x : γ<GOAL>κ.densityProcess κ.fst n a x Set.univ = if (κ.fst a) (MeasurableSpace.countablePartitionSet n x) = 0 then 0 else 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>MeasurableSpace.CountablyGenerated γ<VAR>κ : ProbabilityTheory.Kernel α (γ × β)<VAR>ProbabilityTheory.IsFiniteKernel κ<VAR>n : ℕ<VAR>a : α<GOAL>∀ᵐ (x : γ) ∂κ.fst a, κ.densityProcess κ.fst n a x Set.univ = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>MeasurableSpace.CountablyGenerated γ<VAR>κ : ProbabilityTheory.Kernel α (γ × β)<VAR>n : ℕ<VAR>a : α<VAR>x : γ<VAR>seq : ℕ → Set β<VAR>hseq : Monotone seq<VAR>hseq_iUnion : ⋃ i, seq i = Set.univ<GOAL>Filter.Tendsto (fun m => κ.densityProcess κ.fst n a x (seq m)) Filter.atTop (𝓝 (κ.densityProcess κ.fst n a x Set.univ))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>MeasurableSpace.CountablyGenerated γ<VAR>κ : ProbabilityTheory.Kernel α (γ × β)<VAR>ProbabilityTheory.IsFiniteKernel κ<VAR>n : ℕ<VAR>a : α<VAR>seq : ℕ → Set β<VAR>hseq : Monotone seq<VAR>hseq_iUnion : ⋃ i, seq i = Set.univ<GOAL>∀ᵐ (x : γ) ∂κ.fst a, Filter.Tendsto (fun m => κ.densityProcess κ.fst n a x (seq m)) Filter.atTop (𝓝 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>MeasurableSpace.CountablyGenerated γ<VAR>κ : ProbabilityTheory.Kernel α (γ × β)<VAR>ProbabilityTheory.IsFiniteKernel κ<VAR>a : α<GOAL>∀ᵐ (x : γ) ∂κ.fst a, κ.density κ.fst a x Set.univ = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>MeasurableSpace.CountablyGenerated γ<VAR>κ : ProbabilityTheory.Kernel α (γ × β)<VAR>ProbabilityTheory.IsFiniteKernel κ<VAR>a : α<VAR>seq : ℕ → Set β<VAR>hseq : Monotone seq<VAR>hseq_iUnion : ⋃ i, seq i = Set.univ<VAR>hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)<GOAL>∀ᵐ (x : γ) ∂κ.fst a, Filter.Tendsto (fun m => κ.density κ.fst a x (seq m)) Filter.atTop (𝓝 1)
<VAR>n : ℕ<VAR>x : ℝ<GOAL>deriv^[n] (fun y => Real.exp (-(y ^ 2 / 2))) x = (-1) ^ n * (Polynomial.aeval x) (Polynomial.hermite n) * Real.exp (-(x ^ 2 / 2))
<VAR>n : ℕ<VAR>x : ℝ<GOAL>(Polynomial.aeval x) (Polynomial.hermite n) = (-1) ^ n * deriv^[n] (fun y => Real.exp (-(y ^ 2 / 2))) x / Real.exp (-(x ^ 2 / 2))
<VAR>n : ℕ<VAR>x : ℝ<GOAL>(Polynomial.aeval x) (Polynomial.hermite n) = (-1) ^ n * deriv^[n] (fun y => Real.exp (-(y ^ 2 / 2))) x * Real.exp (x ^ 2 / 2)
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Type u_3<VAR>AddCommGroup N<VAR>Module R N<VAR>f : M →ₗ[R] N<VAR>x : M<GOAL>(LinearMap.reduceModIdealAux I f) (Submodule.Quotient.mk x) = Submodule.Quotient.mk (f x)
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Type u_3<VAR>AddCommGroup N<VAR>Module R N<VAR>f : M →ₗ[R] N<VAR>x : M<GOAL>(LinearMap.reduceModIdeal I f) (Submodule.Quotient.mk x) = Submodule.Quotient.mk (f x)
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Type u_3<VAR>AddCommGroup N<VAR>Module R N<VAR>f : M →ₗ[R] N<VAR>m n : ℕ<VAR>hmn : m ≤ n<GOAL>AdicCompletion.transitionMap I N hmn ∘ₗ ↑R (LinearMap.reduceModIdeal (I ^ n) f) = ↑R (LinearMap.reduceModIdeal (I ^ m) f) ∘ₗ AdicCompletion.transitionMap I M hmn
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Type u_3<VAR>AddCommGroup N<VAR>Module R N<VAR>f : M →ₗ[R] N<VAR>a : AdicCompletion.AdicCauchySequence I M<VAR>n : ℕ<GOAL>↑((AdicCompletion.AdicCauchySequence.map I f) a) n = f (↑a n)
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<GOAL>AdicCompletion.AdicCauchySequence.map I LinearMap.id = LinearMap.id
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Type u_3<VAR>AddCommGroup N<VAR>Module R N<VAR>P : Type u_4<VAR>AddCommGroup P<VAR>Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<GOAL>AdicCompletion.AdicCauchySequence.map I g ∘ₗ AdicCompletion.AdicCauchySequence.map I f = AdicCompletion.AdicCauchySequence.map I (g ∘ₗ f)
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Type u_3<VAR>AddCommGroup N<VAR>Module R N<VAR>P : Type u_4<VAR>AddCommGroup P<VAR>Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>a : AdicCompletion.AdicCauchySequence I M<GOAL>(AdicCompletion.AdicCauchySequence.map I g) ((AdicCompletion.AdicCauchySequence.map I f) a) = (AdicCompletion.AdicCauchySequence.map I (g ∘ₗ f)) a
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Type u_3<VAR>AddCommGroup N<VAR>Module R N<GOAL>AdicCompletion.AdicCauchySequence.map I 0 = 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Type u_3<VAR>AddCommGroup N<VAR>Module R N<VAR>f : M →ₗ[R] N<VAR>n : ℕ<VAR>x : AdicCompletion I M<GOAL>↑((AdicCompletion.adicCompletionAux I f) x) n = (LinearMap.reduceModIdeal (I ^ n) f) (↑x n)
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Type u_3<VAR>AddCommGroup N<VAR>Module R N<VAR>f : M →ₗ[R] N<VAR>n : ℕ<VAR>x : AdicCompletion I M<GOAL>↑((AdicCompletion.map I f) x) n = (LinearMap.reduceModIdeal (I ^ n) f) (↑x n)
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Type u_3<VAR>f g : AdicCompletion I M → N<VAR>h : ∀ (a : AdicCompletion.AdicCauchySequence I M), f ((AdicCompletion.mk I M) a) = g ((AdicCompletion.mk I M) a)<GOAL>f = g
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>T : Type u_5<VAR>AddCommGroup T<VAR>Module (AdicCompletion I R) T<VAR>f g : AdicCompletion I M →ₗ[AdicCompletion I R] T<VAR>h : ∀ (a : AdicCompletion.AdicCauchySequence I M), f ((AdicCompletion.mk I M) a) = g ((AdicCompletion.mk I M) a)<GOAL>f = g
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Type u_3<VAR>AddCommGroup N<VAR>Module R N<VAR>f g : AdicCompletion I M →ₗ[R] N<VAR>h : f ∘ₗ AdicCompletion.mk I M = g ∘ₗ AdicCompletion.mk I M<GOAL>f = g
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<GOAL>AdicCompletion.map I LinearMap.id = LinearMap.id
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Type u_3<VAR>AddCommGroup N<VAR>Module R N<VAR>P : Type u_4<VAR>AddCommGroup P<VAR>Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<GOAL>AdicCompletion.map I g ∘ₗ AdicCompletion.map I f = AdicCompletion.map I (g ∘ₗ f)
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Type u_3<VAR>AddCommGroup N<VAR>Module R N<VAR>P : Type u_4<VAR>AddCommGroup P<VAR>Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>x : AdicCompletion I M<GOAL>(AdicCompletion.map I g) ((AdicCompletion.map I f) x) = (AdicCompletion.map I (g ∘ₗ f)) x
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Type u_3<VAR>AddCommGroup N<VAR>Module R N<VAR>f : M →ₗ[R] N<VAR>a : AdicCompletion.AdicCauchySequence I M<GOAL>(AdicCompletion.map I f) ((AdicCompletion.mk I M) a) = (AdicCompletion.mk I N) ((AdicCompletion.AdicCauchySequence.map I f) a)
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Type u_3<VAR>AddCommGroup N<VAR>Module R N<GOAL>AdicCompletion.map I 0 = 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Type u_3<VAR>AddCommGroup N<VAR>Module R N<VAR>f : M ≃ₗ[R] N<VAR>x : AdicCompletion I M<GOAL>(AdicCompletion.congr I f) x = (AdicCompletion.map I ↑f) x
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Type u_3<VAR>AddCommGroup N<VAR>Module R N<VAR>f : M ≃ₗ[R] N<VAR>x : AdicCompletion I N<GOAL>(AdicCompletion.congr I f).symm x = (AdicCompletion.map I ↑f.symm) x
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>ι : Type u_6<VAR>M : ι → Type u_7<VAR>(i : ι) → AddCommGroup (M i)<VAR>(i : ι) → Module R (M i)<VAR>c : AdicCompletion I ((j : ι) → M j)<VAR>i : ι<VAR>n : ℕ<GOAL>↑((AdicCompletion.pi I M) c i) n = (LinearMap.reduceModIdeal (I ^ n) (LinearMap.proj i)) (↑c n)
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>ι : Type u_6<VAR>DecidableEq ι<VAR>M : ι → Type u_7<VAR>(i : ι) → AddCommGroup (M i)<VAR>(i : ι) → Module R (M i)<VAR>j : ι<VAR>x : AdicCompletion I (M j)<GOAL>(AdicCompletion.sum I M) ((DirectSum.lof (AdicCompletion I R) ι (fun i => AdicCompletion I (M i)) j) x) = (AdicCompletion.map I (DirectSum.lof R ι M j)) x
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>ι : Type u_6<VAR>DecidableEq ι<VAR>M : ι → Type u_7<VAR>(i : ι) → AddCommGroup (M i)<VAR>(i : ι) → Module R (M i)<VAR>j : ι<VAR>x : AdicCompletion I (M j)<GOAL>(AdicCompletion.sum I M) ((DirectSum.of (fun i => AdicCompletion I (M i)) j) x) = (AdicCompletion.map I (DirectSum.lof R ι M j)) x
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>ι : Type u_6<VAR>M : ι → Type u_7<VAR>(i : ι) → AddCommGroup (M i)<VAR>(i : ι) → Module R (M i)<VAR>Fintype ι<VAR>x : AdicCompletion I (DirectSum ι fun j => M j)<VAR>j : ι<GOAL>(DirectSum.component (AdicCompletion I R) ι (fun i => AdicCompletion I (M i)) j) ((AdicCompletion.sumInv I M) x) = (AdicCompletion.map I (DirectSum.component R ι M j)) x
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>ι : Type u_6<VAR>M : ι → Type u_7<VAR>(i : ι) → AddCommGroup (M i)<VAR>(i : ι) → Module R (M i)<VAR>Fintype ι<VAR>x : AdicCompletion I (DirectSum ι fun j => M j)<VAR>j : ι<GOAL>((AdicCompletion.sumInv I M) x) j = (AdicCompletion.map I (DirectSum.component R ι M j)) x
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>ι : Type u_6<VAR>DecidableEq ι<VAR>M : ι → Type u_7<VAR>(i : ι) → AddCommGroup (M i)<VAR>(i : ι) → Module R (M i)<VAR>Fintype ι<GOAL>AdicCompletion.sumInv I M ∘ₗ AdicCompletion.sum I M = LinearMap.id
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>ι : Type u_6<VAR>DecidableEq ι<VAR>M : ι → Type u_7<VAR>(i : ι) → AddCommGroup (M i)<VAR>(i : ι) → Module R (M i)<VAR>Fintype ι<GOAL>AdicCompletion.sum I M ∘ₗ AdicCompletion.sumInv I M = LinearMap.id
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>ι : Type u_6<VAR>DecidableEq ι<VAR>M : ι → Type u_7<VAR>(i : ι) → AddCommGroup (M i)<VAR>(i : ι) → Module R (M i)<VAR>Fintype ι<VAR>x : DirectSum ι fun j => AdicCompletion I (M j)<GOAL>(AdicCompletion.sumEquivOfFintype I M) x = (AdicCompletion.sum I M) x
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>ι : Type u_6<VAR>DecidableEq ι<VAR>M : ι → Type u_7<VAR>(i : ι) → AddCommGroup (M i)<VAR>(i : ι) → Module R (M i)<VAR>Fintype ι<VAR>x : AdicCompletion I (DirectSum ι fun j => M j)<GOAL>(AdicCompletion.sumEquivOfFintype I M).symm x = (AdicCompletion.sumInv I M) x
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>ι : Type u_6<VAR>DecidableEq ι<VAR>M : ι → Type u_7<VAR>(i : ι) → AddCommGroup (M i)<VAR>(i : ι) → Module R (M i)<VAR>Fintype ι<VAR>x : AdicCompletion I ((j : ι) → M j)<GOAL>(AdicCompletion.piEquivOfFintype I M) x = (AdicCompletion.pi I M) x
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>n : ℕ<VAR>x : AdicCompletion I (Fin n → R)<GOAL>(AdicCompletion.piEquivFin I n) x = (AdicCompletion.pi I fun x => R) x
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>m n : ℕ<VAR>hmn : m ≤ n<VAR>x : R<GOAL>(AdicCompletion.transitionMap I R hmn) ((Ideal.Quotient.mk (I ^ n • ⊤)) x) = (Ideal.Quotient.mk (I ^ m • ⊤)) x
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>m n : ℕ<VAR>hmn : m ≤ n<GOAL>(AdicCompletion.transitionMap I R hmn) 1 = 1
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>m n : ℕ<VAR>hmn : m ≤ n<VAR>x : R ⧸ I ^ n • ⊤<VAR>y : R ⧸ I ^ n • ⊤<GOAL>(AdicCompletion.transitionMap I R hmn) (x * y) = (AdicCompletion.transitionMap I R hmn) x * (AdicCompletion.transitionMap I R hmn) y