-
Notifications
You must be signed in to change notification settings - Fork 251
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - fix: Incorrect integral curve existence theorem for vector fields #6875
Conversation
split_ifs with h | ||
· rwa [← h] at hr' | ||
· exact (mul_div_cancel' (r / 2) h).le } | ||
#align exists_is_picard_lindelof_const_of_cont_diff_on_nhds exists_isPicardLindelof_const_of_contDiffOn_nhds |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
You should not delete #aligns (same below)
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
What if the theorem name and statement have changed?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I would still keep the #align
.
∃ f : ℝ → E, f t₀ = x₀ ∧ ∀ t ∈ Ioo (t₀ - ε) (t₀ + ε), f t ∈ s ∧ HasDerivAt f (v (f t)) t := by | ||
obtain ⟨ε, hε, L, R, C, hpl⟩ := exists_isPicardLindelof_const_of_contDiffOn_nhds t₀ x₀ hv hs |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I might be very stupid here, but it seems to me that your version is less strong in the sense that you don't have control over the image of f
?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think it's my original statement of the theorem that was a bit stupid. Since f
is differentiable at t₀
, you can just shrink ε
until f t ∈ s
for any s ∈ nhds x₀
.
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
The new statements are a lot nicer! Please add back the bors d+ |
✌️ winstonyin can now approve this pull request. To approve and merge a pull request, simply reply with |
bors r+ |
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
exists_isPicardLindelof_const_of_contDiffOn_nhds
had unnecessarily specific assumptions.ContDiffOn
assumption is replaced withContDiffAt
.ProperSpace E
assumption is removed.