feat(data/complex/exponential): exp, sin, cos, arcsin etc.#386
feat(data/complex/exponential): exp, sin, cos, arcsin etc.#386johoelzl merged 56 commits intoleanprover-community:masterfrom
Conversation
nential function
| open real | ||
|
|
||
| lemma real.intermediate_value {f : ℝ → ℝ} {a b t : ℝ} | ||
| (hf : ∀ x, a ≤ x → x ≤ b → tendsto f (nhds x) (nhds (f x))) |
There was a problem hiding this comment.
You are assuming full continuity at a and b instead of one-sided continuity (i.e., continuity within [a,b]), that would be the natural condition here.
There was a problem hiding this comment.
what @sgouezel wants is:
hf : ∀ x, a ≤ x → x ≤ b → tendsto f (inf (nhds x) (principal (Icc a b))) (nhds (f x))
There was a problem hiding this comment.
@johoelzl What do you think of defining a filter nhds_within S x = inf (nhds x) (principal S) and use it to define continuity within S (not in this pull request, of course!). Or is it better design to always go first to the subtype S and then use nhds x for the induced topology? (Of course, the two are equivalent). With my Isabelle-biased point of view, I tend to prefer the first approach, avoiding subtypes when possible.
There was a problem hiding this comment.
My hope is that the subtype approach is working. So also here it would be an option to write:
hf : ∀ x:Icc a b, tendsto (λx:Icc a b, f x.1) (nhds x) (nhds (f x.1))
There was a problem hiding this comment.
I think if you really want to pursue this route you should just treat Icc a b as a topological space in its own right, and f is a continuous function on that domain. We will probably need a lot of lemmas about the unit interval as a topological space anyway, since it plays so prominently in path connectedness and the fundamental group.
|
@dorhinj Up to now, I only was roughly going over this PR. Its amazing! |
analysis/exponential.lean
Outdated
|
|
||
| open finset filter | ||
|
|
||
| #print classical.em |
There was a problem hiding this comment.
Oups, it is already removed in the next commit. Forget it!
|
I'm fine with merging this. My biggest critique is that it develops quiet some theory around Cauchy limits instead of using topological limits. But it sounds Mario wants to have it that way. Anything against merging it now? It is quiet big and has often merge conflicts, so I would prefer to merge it now. |
This PR includes definitions for
exp,sin,cos,tan,sinh,coshandtanh, andlogon complex numbers and reals. There are two large files created,data/complex/exponentialandanalysis/exponential. The latter file contains all the definitions that depend on continuity.arcsin,arccos, andarctanon realspiargfunction on complex numbers.the intermediate value theorem on reals.
One other point is that I changed the definition of
floor_ring, fromextends linear_ordered_ring, to taking[linear_ordered_ring α]as an argument, since I proved lemmas true in a floor field, and didn't want to create afloor_fieldclass.TO CONTRIBUTORS:
Make sure you have:
For reviewers: code review check list