Skip to content

Commit 8495ce1

Browse files
bmtragerbmtrager
committed
Update Rocq 9 imports
1 parent 4cbd9db commit 8495ce1

23 files changed

Lines changed: 1389 additions & 18 deletions

‎Makefile.coq‎

Lines changed: 989 additions & 0 deletions
Large diffs are not rendered by default.

‎Makefile.coq.conf‎

Lines changed: 71 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,71 @@
1+
# This configuration file was generated by running:
2+
# coq_makefile -f _CoqProject coq/lib_utils/LibUtilsAssoc.v coq/lib_utils/LibUtilsBag.v coq/lib_utils/LibUtilsBindings.v coq/lib_utils/LibUtilsBindingsNat.v coq/lib_utils/LibUtilsClosure.v coq/lib_utils/LibUtilsCompat.v coq/lib_utils/LibUtilsCoqLibAdd.v coq/lib_utils/LibUtilsDigits.v coq/lib_utils/LibUtilsFresh.v coq/lib_utils/LibUtilsGroupByDomain.v coq/lib_utils/LibUtilsInterleaved.v coq/lib_utils/LibUtilsLattice.v coq/lib_utils/LibUtilsLift.v coq/lib_utils/LibUtilsLiftIterators.v coq/lib_utils/LibUtilsListAdd.v coq/lib_utils/LibUtilsResult.v coq/lib_utils/LibUtilsSortingAdd.v coq/lib_utils/LibUtilsStringAdd.v coq/lib_utils/LibUtilsSublist.v coq/lib_utils/LibUtils.v coq/CertRL/LM/R_compl.v coq/CertRL/LM/check_sub_structure.v coq/CertRL/LM/compatible.v coq/CertRL/LM/continuous_linear_map.v coq/CertRL/LM/fixed_point.v coq/CertRL/LM/hierarchyD.v coq/CertRL/LM/hilbert.v coq/CertRL/LM/linear_map.v coq/CertRL/LM/logic_tricks.v coq/CertRL/LM/lax_milgram.v coq/CertRL/LM/lax_milgram_cea.v coq/utils/BasicUtils.v coq/utils/Assoc.v coq/utils/ClassicUtils.v coq/utils/CoquelicotAdd.v coq/utils/ELim_Seq.v coq/utils/ExtrFloatishIEEE.v coq/utils/improper_integrals.v coq/utils/Isomorphism.v coq/utils/ListAdd.v coq/utils/FiniteType.v coq/utils/FiniteTypeVector.v coq/utils/NumberIso.v coq/utils/PairEncoding.v coq/utils/Quotient.v coq/utils/quotient_space.v coq/utils/RealAdd.v coq/utils/RbarAdd.v coq/utils/RiemannAdd.v coq/utils/StreamAdd.v coq/utils/StreamLimits.v coq/utils/Sums.v coq/utils/nvector.v coq/utils/Vector.v coq/utils/PushNeg.v coq/utils/DVector.v coq/utils/Utils.v coq/utils/Floatish/FloatishDef.v coq/utils/Floatish/FloatishOps.v coq/utils/Floatish/FloatishRealOps.v coq/utils/Floatish/FloatishInterval.v coq/utils/Floatish/FloatishIEEE.v coq/utils/Floatish/FloatishReal.v coq/utils/Floatish.v coq/NeuralNetworks/AxiomaticNormedRealVectorSpace.v coq/NeuralNetworks/DefinedFunctions.v coq/NeuralNetworks/derivlemmas.v coq/NeuralNetworks/Gen_NN.v coq/ProbTheory/Almost.v coq/ProbTheory/BorelSigmaAlgebra.v coq/ProbTheory/DiscreteProbSpace.v coq/ProbTheory/Dynkin.v coq/ProbTheory/Event.v coq/ProbTheory/Independence.v coq/ProbTheory/ProbSpace.v coq/ProbTheory/FunctionsToReal.v coq/ProbTheory/Measures.v coq/ProbTheory/RandomVariable.v coq/ProbTheory/RealRandomVariable.v coq/ProbTheory/RandomVariableFinite.v coq/ProbTheory/RandomVariableL2.v coq/ProbTheory/RandomVariableLpNat.v coq/ProbTheory/RandomVariableLpR.v coq/ProbTheory/RandomVariableLinf.v coq/ProbTheory/OrthoProject.v coq/ProbTheory/RealVectorHilbert.v coq/ProbTheory/SimpleExpectation.v coq/ProbTheory/ConditionalExpectation.v coq/ProbTheory/Expectation.v coq/ProbTheory/RbarExpectation.v coq/ProbTheory/VectorConditionalExpectation.v coq/ProbTheory/SigmaAlgebras.v coq/ProbTheory/VectorRandomVariable.v coq/ProbTheory/Martingale.v coq/ProbTheory/MartingaleConvergence.v coq/ProbTheory/MartingaleStopped.v coq/ProbTheory/Gaussian.v coq/ProbTheory/ProductSpace.v coq/ProbTheory/ProductSpaceDep.v coq/CertRL/pmf_monad.v coq/CertRL/qvalues.v coq/CertRL/mdp.v coq/CertRL/mdp_turtle.v coq/CertRL/finite_time.v coq/CertRL/cond_expt.v coq/CertRL/pmf_prob.v coq/QLearn/Dvoretzky.v coq/QLearn/Bellman.v coq/QLearn/qlearn_aux.v coq/QLearn/qlearn.v coq/QLearn/qlearn_redux.v coq/QLearn/infprod.v coq/QLearn/sumtest.v coq/QLearn/slln.v coq/QLearn/vecslln.v coq/QLearn/uniform_converge.v coq/QLearn/lim_add.v coq/QLearn/Tsitsiklis.v coq/QLearn/jaakkola_vector.v coq/FHE/nth_root.v coq/FHE/encode.v coq/FHE/encrypt.v coq/FHE/zp_prim_root.v coq/FHE/arith.v coq/API.v -o Makefile.coq
3+
4+
COQBIN?=
5+
ifneq (,$(COQBIN))
6+
# add an ending /
7+
COQBIN:=$(COQBIN)/
8+
endif
9+
COQMKFILE ?= "$(COQBIN)coq_makefile"
10+
11+
###############################################################################
12+
# #
13+
# Project files. #
14+
# #
15+
###############################################################################
16+
17+
COQMF_CMDLINE_VFILES := coq/lib_utils/LibUtilsAssoc.v coq/lib_utils/LibUtilsBag.v coq/lib_utils/LibUtilsBindings.v coq/lib_utils/LibUtilsBindingsNat.v coq/lib_utils/LibUtilsClosure.v coq/lib_utils/LibUtilsCompat.v coq/lib_utils/LibUtilsCoqLibAdd.v coq/lib_utils/LibUtilsDigits.v coq/lib_utils/LibUtilsFresh.v coq/lib_utils/LibUtilsGroupByDomain.v coq/lib_utils/LibUtilsInterleaved.v coq/lib_utils/LibUtilsLattice.v coq/lib_utils/LibUtilsLift.v coq/lib_utils/LibUtilsLiftIterators.v coq/lib_utils/LibUtilsListAdd.v coq/lib_utils/LibUtilsResult.v coq/lib_utils/LibUtilsSortingAdd.v coq/lib_utils/LibUtilsStringAdd.v coq/lib_utils/LibUtilsSublist.v coq/lib_utils/LibUtils.v coq/CertRL/LM/R_compl.v coq/CertRL/LM/check_sub_structure.v coq/CertRL/LM/compatible.v coq/CertRL/LM/continuous_linear_map.v coq/CertRL/LM/fixed_point.v coq/CertRL/LM/hierarchyD.v coq/CertRL/LM/hilbert.v coq/CertRL/LM/linear_map.v coq/CertRL/LM/logic_tricks.v coq/CertRL/LM/lax_milgram.v coq/CertRL/LM/lax_milgram_cea.v coq/utils/BasicUtils.v coq/utils/Assoc.v coq/utils/ClassicUtils.v coq/utils/CoquelicotAdd.v coq/utils/ELim_Seq.v coq/utils/ExtrFloatishIEEE.v coq/utils/improper_integrals.v coq/utils/Isomorphism.v coq/utils/ListAdd.v coq/utils/FiniteType.v coq/utils/FiniteTypeVector.v coq/utils/NumberIso.v coq/utils/PairEncoding.v coq/utils/Quotient.v coq/utils/quotient_space.v coq/utils/RealAdd.v coq/utils/RbarAdd.v coq/utils/RiemannAdd.v coq/utils/StreamAdd.v coq/utils/StreamLimits.v coq/utils/Sums.v coq/utils/nvector.v coq/utils/Vector.v coq/utils/PushNeg.v coq/utils/DVector.v coq/utils/Utils.v coq/utils/Floatish/FloatishDef.v coq/utils/Floatish/FloatishOps.v coq/utils/Floatish/FloatishRealOps.v coq/utils/Floatish/FloatishInterval.v coq/utils/Floatish/FloatishIEEE.v coq/utils/Floatish/FloatishReal.v coq/utils/Floatish.v coq/NeuralNetworks/AxiomaticNormedRealVectorSpace.v coq/NeuralNetworks/DefinedFunctions.v coq/NeuralNetworks/derivlemmas.v coq/NeuralNetworks/Gen_NN.v coq/ProbTheory/Almost.v coq/ProbTheory/BorelSigmaAlgebra.v coq/ProbTheory/DiscreteProbSpace.v coq/ProbTheory/Dynkin.v coq/ProbTheory/Event.v coq/ProbTheory/Independence.v coq/ProbTheory/ProbSpace.v coq/ProbTheory/FunctionsToReal.v coq/ProbTheory/Measures.v coq/ProbTheory/RandomVariable.v coq/ProbTheory/RealRandomVariable.v coq/ProbTheory/RandomVariableFinite.v coq/ProbTheory/RandomVariableL2.v coq/ProbTheory/RandomVariableLpNat.v coq/ProbTheory/RandomVariableLpR.v coq/ProbTheory/RandomVariableLinf.v coq/ProbTheory/OrthoProject.v coq/ProbTheory/RealVectorHilbert.v coq/ProbTheory/SimpleExpectation.v coq/ProbTheory/ConditionalExpectation.v coq/ProbTheory/Expectation.v coq/ProbTheory/RbarExpectation.v coq/ProbTheory/VectorConditionalExpectation.v coq/ProbTheory/SigmaAlgebras.v coq/ProbTheory/VectorRandomVariable.v coq/ProbTheory/Martingale.v coq/ProbTheory/MartingaleConvergence.v coq/ProbTheory/MartingaleStopped.v coq/ProbTheory/Gaussian.v coq/ProbTheory/ProductSpace.v coq/ProbTheory/ProductSpaceDep.v coq/CertRL/pmf_monad.v coq/CertRL/qvalues.v coq/CertRL/mdp.v coq/CertRL/mdp_turtle.v coq/CertRL/finite_time.v coq/CertRL/cond_expt.v coq/CertRL/pmf_prob.v coq/QLearn/Dvoretzky.v coq/QLearn/Bellman.v coq/QLearn/qlearn_aux.v coq/QLearn/qlearn.v coq/QLearn/qlearn_redux.v coq/QLearn/infprod.v coq/QLearn/sumtest.v coq/QLearn/slln.v coq/QLearn/vecslln.v coq/QLearn/uniform_converge.v coq/QLearn/lim_add.v coq/QLearn/Tsitsiklis.v coq/QLearn/jaakkola_vector.v coq/FHE/nth_root.v coq/FHE/encode.v coq/FHE/encrypt.v coq/FHE/zp_prim_root.v coq/FHE/arith.v coq/API.v
18+
COQMF_SOURCES := $(shell $(COQMKFILE) -sources-of -f _CoqProject $(COQMF_CMDLINE_VFILES))
19+
COQMF_VFILES := $(filter %.v, $(COQMF_SOURCES))
20+
COQMF_MLIFILES := $(filter %.mli, $(COQMF_SOURCES))
21+
COQMF_MLFILES := $(filter %.ml, $(COQMF_SOURCES))
22+
COQMF_MLGFILES := $(filter %.mlg, $(COQMF_SOURCES))
23+
COQMF_MLPACKFILES := $(filter %.mlpack, $(COQMF_SOURCES))
24+
COQMF_MLLIBFILES := $(filter %.mllib, $(COQMF_SOURCES))
25+
COQMF_METAFILE =
26+
27+
###############################################################################
28+
# #
29+
# Path directives (-I, -R, -Q). #
30+
# #
31+
###############################################################################
32+
33+
COQMF_OCAMLLIBS =
34+
COQMF_SRC_SUBDIRS =
35+
COQMF_COQLIBS = -R coq FormalML
36+
COQMF_COQLIBS_NOML = -R coq FormalML
37+
COQMF_CMDLINE_COQLIBS =
38+
39+
###############################################################################
40+
# #
41+
# Coq configuration. #
42+
# #
43+
###############################################################################
44+
45+
COQMF_COQLIB=/Users/bmt/.opam/default/lib/coq/
46+
COQMF_COQCORELIB=/Users/bmt/.opam/default/lib/coq/../coq-core/
47+
COQMF_DOCDIR=/Users/bmt/.opam/default/share/doc/
48+
COQMF_OCAMLFIND=/Users/bmt/.opam/default/bin/ocamlfind
49+
COQMF_CAMLFLAGS=-thread -bin-annot -strict-sequence -w -a+1..3-4+5..8-9+10..26-27+28..39-40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70
50+
COQMF_WARN=-warn-error +a-3
51+
COQMF_HASNATDYNLINK=true
52+
COQMF_COQ_SRC_SUBDIRS=boot config lib clib kernel library engine pretyping interp gramlib parsing proofs tactics toplevel printing ide stm vernac plugins/btauto plugins/cc plugins/derive plugins/extraction plugins/firstorder plugins/funind plugins/ltac plugins/ltac2 plugins/micromega plugins/nsatz plugins/ring plugins/rtauto plugins/ssr plugins/ssrmatching plugins/syntax
53+
COQMF_COQ_NATIVE_COMPILER_DEFAULT=no
54+
COQMF_WINDRIVE=
55+
56+
###############################################################################
57+
# #
58+
# Native compiler. #
59+
# #
60+
###############################################################################
61+
62+
COQMF_COQPROJECTNATIVEFLAG =
63+
64+
###############################################################################
65+
# #
66+
# Extra variables. #
67+
# #
68+
###############################################################################
69+
70+
COQMF_OTHERFLAGS = '-set' 'Warnings=+default,-ambiguous-path,-coercions,-hiding-delimiting-key,-overwriting-delimiting-key,-redundant-canonical-projection,-typechecker,-ssr-search-moved,-deprecated,-notation-overridden'
71+
COQMF_INSTALLCOQDOCROOT = FormalML

‎coq/FHE/nth_root.lean‎

Lines changed: 86 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,86 @@
1+
import Mathlib.RingTheory.RootsOfUnity.Complex
2+
3+
open Classical Nat Real Complex
4+
5+
noncomputable section
6+
7+
def nth_root (j n : Nat) :=
8+
(exp (2 * ↑Real.pi * I * (↑j / ↑n)))
9+
10+
theorem nth_root_0 n :
11+
nth_root 0 (succ n) = 1 := by
12+
unfold nth_root
13+
simp
14+
15+
theorem nth_root_2PI_1 n :
16+
nth_root (succ n) (succ n) = 1 := by
17+
unfold nth_root
18+
rw [div_eq_mul_inv]
19+
rw [Complex.mul_inv_cancel]
20+
. rw [mul_one]
21+
rw [Complex.exp_eq_one_iff]
22+
exists 1
23+
simp
24+
. rw [cast_ne_zero]
25+
apply succ_ne_zero
26+
27+
theorem nth_root_2PI j n :
28+
nth_root (j * (succ n)) (succ n) = 1 := by
29+
unfold nth_root
30+
rw [Complex.exp_eq_one_iff]
31+
exists j
32+
rw [div_eq_mul_inv]
33+
rw [Nat.cast_mul]
34+
rw [mul_assoc (@Nat.cast _ _ j)]
35+
rw [Complex.mul_inv_cancel]
36+
. simp; ring
37+
. rw [cast_ne_zero]
38+
apply succ_ne_zero
39+
40+
theorem nth_root_2PI_plus n j k :
41+
nth_root (j + k * (succ n)) (succ n) = nth_root j (succ n) := by
42+
unfold nth_root
43+
rw [Complex.exp_eq_exp_iff_exists_int]
44+
exists k
45+
rw [div_eq_mul_inv]
46+
rw [cast_add, add_mul, cast_mul]
47+
rw [mul_assoc (@Nat.cast _ _ k)]
48+
rw [Complex.mul_inv_cancel]
49+
. simp; ring
50+
. rw [cast_ne_zero]
51+
apply succ_ne_zero
52+
53+
theorem pow_nth_root j n e :
54+
(nth_root j (succ n)) ^ e = nth_root (e * j) (succ n) := by
55+
unfold nth_root
56+
rw [← Complex.exp_nat_mul, Complex.exp_eq_exp_iff_exists_int]
57+
exists 0
58+
rw [Int.cast_zero, zero_mul, add_zero]
59+
simp; ring
60+
61+
theorem pow_nth_root_comm j n e :
62+
(nth_root j (succ n)) ^ e = (nth_root e (succ n)) ^ j := by
63+
rw [pow_nth_root]
64+
rw [pow_nth_root]
65+
rw [mul_comm]
66+
67+
theorem nth_root_npow j n :
68+
(nth_root j (succ n)) ^ (succ n) = 1 := by
69+
rw [pow_nth_root, mul_comm, nth_root_2PI]
70+
71+
theorem prim_nth_root j n :
72+
nth_root j (succ n) = (nth_root 1 (succ n)) ^ j := by
73+
rw [pow_nth_root]
74+
simp
75+
76+
77+
78+
79+
80+
81+
82+
83+
84+
85+
86+

‎coq/FHE/nth_root.lean~‎

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
import Mathlib.RingTheory.RootsOfUnity.Complex
2+
3+
open Classical
4+
open Complex
5+
6+
noncomputable section
7+
8+
def nth_root (j n : Nat) :=
9+
(exp (2 * ↑Real.pi * I * (↑j / ↑n)))
10+
11+
theorem nth_root_0 n :
12+
nth_root 0 (Nat.succ n) = 1 := by
13+
unfold nth_root
14+
simp
15+
16+
theorem nth_root_2PI n j :
17+
nth_root (j * (S n)) (S n) = 1.

‎coq/FHE/nth_root_new.lean‎

Lines changed: 99 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,99 @@
1+
import Mathlib.RingTheory.RootsOfUnity.Complex
2+
3+
open Classical Nat Real Complex
4+
5+
noncomputable section
6+
7+
def nth_root (j n : Nat) :=
8+
(exp (2 * ↑Real.pi * I * (↑j / ↑n)))
9+
10+
theorem nth_root_0 n :
11+
nth_root 0 (succ n) = 1 := by
12+
unfold nth_root
13+
simp
14+
15+
theorem nth_root_2PI_1 n :
16+
nth_root (succ n) (succ n) = 1 := by
17+
unfold nth_root
18+
rw [div_eq_mul_inv]
19+
rw [Complex.mul_inv_cancel]
20+
. rw [mul_one]
21+
rw [Complex.exp_eq_one_iff]
22+
exists 1
23+
simp
24+
. rw [cast_ne_zero]
25+
apply succ_ne_zero
26+
27+
28+
theorem nth_root_2PI j n :
29+
nth_root (j * (succ n)) (succ n) = 1 := by
30+
unfold nth_root
31+
rw [Complex.exp_eq_one_iff]
32+
exists j
33+
rw [div_eq_mul_inv]
34+
rw [cast_mul]
35+
rw [mul_assoc]
36+
rw [mul_assoc]
37+
rw [mul_assoc]
38+
rw [Complex.mul_inv_cancel]
39+
. rw [mul_one]
40+
simp; ring
41+
. rw [cast_ne_zero]
42+
apply succ_ne_zero
43+
44+
45+
theorem nth_root_2PI_plus n j k :
46+
nth_root (j + k * (succ n)) (succ n) = nth_root j (succ n) := by
47+
unfold nth_root
48+
rw [Complex.exp_eq_exp_iff_exists_int]
49+
exists k
50+
rw [div_eq_mul_inv]
51+
rw [mul_assoc]
52+
rw [mul_assoc]
53+
rw [cast_add]
54+
rw [add_mul]
55+
rw [mul_assoc]
56+
rw [cast_mul]
57+
rw [mul_assoc]
58+
rw [Complex.mul_inv_cancel]
59+
. simp; ring
60+
. rw [cast_ne_zero]
61+
apply succ_ne_zero
62+
63+
64+
theorem pow_nth_root j n e :
65+
(nth_root j (succ n)) ^ e = nth_root (e * j) (succ n) := by
66+
unfold nth_root
67+
rw [← Complex.exp_nat_mul]
68+
rw [Complex.exp_eq_exp_iff_exists_int]
69+
exists 0
70+
rw [Int.cast_zero]
71+
rw [zero_mul]
72+
rw [add_zero]
73+
simp; ring
74+
75+
theorem pow_nth_root_comm j n e :
76+
(nth_root j (succ n)) ^ e = (nth_root e (succ n)) ^ j := by
77+
rw [pow_nth_root]
78+
rw [pow_nth_root]
79+
rw [mul_comm]
80+
81+
theorem nth_root_npow j n :
82+
(nth_root j (succ n)) ^ (succ n) = 1 := by
83+
rw [pow_nth_root, mul_comm, nth_root_2PI]
84+
85+
86+
theorem prim_nth_root j n :
87+
nth_root j (succ n) = (nth_root 1 (succ n)) ^ j := by
88+
rw [pow_nth_root]
89+
simp
90+
91+
92+
93+
94+
95+
96+
97+
98+
99+

‎coq/FHE/nth_root_new.lean~‎

Lines changed: 102 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,102 @@
1+
import Mathlib.RingTheory.RootsOfUnity.Complex
2+
3+
open Classical Nat Real Complex
4+
5+
noncomputable section
6+
7+
def nth_root (j n : Nat) :=
8+
(exp (2 * ↑Real.pi * I * (↑j / ↑n)))
9+
10+
theorem nth_root_0 n :
11+
nth_root 0 (succ n) = 1 := by
12+
unfold nth_root
13+
simp
14+
15+
theorem nth_root_2PI_1 n :
16+
nth_root (succ n) (succ n) = 1 := by
17+
unfold nth_root
18+
rw [div_eq_mul_inv]
19+
rw [Complex.mul_inv_cancel]
20+
. rw [mul_one]
21+
rw [Complex.exp_eq_one_iff]
22+
exists 1
23+
simp
24+
. rw [cast_ne_zero]
25+
apply succ_ne_zero
26+
27+
28+
theorem nth_root_2PI j n :
29+
nth_root (j * (succ n)) (succ n) = 1 := by
30+
unfold nth_root
31+
rw [Complex.exp_eq_one_iff]
32+
exists j
33+
rw [div_eq_mul_inv]
34+
rw [Nat.cast_mul]
35+
rw [mul_assoc]
36+
rw [mul_assoc]
37+
rw [mul_assoc]
38+
rw [Complex.mul_inv_cancel]
39+
. rw [mul_one]
40+
simp
41+
ring
42+
. rw [Nat.cast_ne_zero]
43+
apply Nat.succ_ne_zero
44+
45+
46+
theorem nth_root_2PI_plus n j k :
47+
nth_root (j + k * (succ n)) (succ n) = nth_root j (succ n) := by
48+
unfold nth_root
49+
rw [Complex.exp_eq_exp_iff_exists_int]
50+
exists k
51+
rw [div_eq_mul_inv]
52+
rw [mul_assoc]
53+
rw [mul_assoc]
54+
rw [Nat.cast_add]
55+
rw [add_mul]
56+
rw [mul_assoc]
57+
rw [Nat.cast_mul]
58+
rw [mul_assoc]
59+
rw [Complex.mul_inv_cancel]
60+
. simp
61+
ring
62+
. rw [Nat.cast_ne_zero]
63+
apply Nat.succ_ne_zero
64+
65+
66+
theorem pow_nth_root j n e :
67+
(nth_root j (succ n)) ^ e = nth_root (e * j) (succ n) := by
68+
unfold nth_root
69+
rw [← Complex.exp_nat_mul]
70+
rw [Complex.exp_eq_exp_iff_exists_int]
71+
exists 0
72+
rw [Int.cast_zero]
73+
rw [zero_mul]
74+
rw [add_zero]
75+
simp
76+
ring
77+
78+
theorem pow_nth_root_comm j n e :
79+
(nth_root j (succ n)) ^ e = (nth_root e (succ n)) ^ j := by
80+
rw [pow_nth_root]
81+
rw [pow_nth_root]
82+
rw [mul_comm]
83+
84+
theorem nth_root_npow j n :
85+
(nth_root j (succ n)) ^ (succ n) = 1 := by
86+
rw [pow_nth_root, mul_comm, nth_root_2PI]
87+
88+
89+
theorem prim_nth_root j n :
90+
nth_root j (succ n) = (nth_root 1 (succ n)) ^ j := by
91+
rw [pow_nth_root]
92+
simp
93+
94+
95+
96+
97+
98+
99+
100+
101+
102+

‎docs/1051027873.pdf‎

169 KB
Binary file not shown.

‎docs/11492793.pdf‎

848 KB
Binary file not shown.

‎docs/2202.05959.pdf‎

792 KB
Binary file not shown.

‎docs/Dvoretzky - ON STOCHASTIC APPROXIMATION.pdf‎

982 KB
Binary file not shown.

0 commit comments

Comments
 (0)