feat(measure_theory): prove that the Giry monad is a monad in the category_theory sense #1259
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
|
Looks great. It seems like it wasn’t too painful either, and that the new |
jcommelin
reviewed
Jul 24, 2019
…egory_theory sense
|
I tend to:
1. Write out all the fields, filled in with sorry (including the auto_param
fields).
2. Fill in the meaningful data fields.
3. Try removing the auto_param fields one by one, to see which ones the
tactic can handle.
4. Write any remaining proofs.
It's certainly an unfortunate problem that while the data fields are
incomplete or broken, Lean wastes a lot of time running auto_param tactics.
…On Wed, Jul 24, 2019, 3:52 PM Johannes Hölzl ***@***.***> wrote:
***@***.**** commented on this pull request.
------------------------------
In src/measure_theory/Meas.lean
<#1259 (comment)>
:
> @@ -24,6 +27,34 @@ def of (X : Type u) [measurable_space X] : Meas := ⟨X⟩
-- -- If `measurable` were a class, we would summon instances:
-- local attribute [class] measurable
-- instance {X Y : Meas} (f : X ⟶ Y) : measurable (f : X → Y) := f.2
+
+def Measure : Meas ⥤ Meas :=
+⟨ λX, ***@***.***_theory.measure X.1 X.2⟩,
True, but there are two problems:
1. Lean was crashing when writing down the structure syntax (some
assertions), and
2. the auto-parameters took ages to fail
I can use the structure syntax again.
—
You are receiving this because you commented.
Reply to this email directly, view it on GitHub
<#1259?email_source=notifications&email_token=AADUWBFBW27T7R234FDOZA3QA7U2NA5CNFSM4IGKCEOKYY3PNVWWK3TUL52HS4DFWFIHK3DMKJSXC5LFON2FEZLWNFSXPKTDN5WW2ZLOORPWSZGOB7L5NGQ#discussion_r306636733>,
or mute the thread
<https://github.com/notifications/unsubscribe-auth/AADUWBAIX7HQDMHH6GHU7GTQA7U2NANCNFSM4IGKCEOA>
.
|
jcommelin
reviewed
Jul 24, 2019
jcommelin
reviewed
Jul 24, 2019
|
A third problem I have with the structure notation: |
|
Could you add module documentation for |
robertylewis
added
the
needs-documentation
rwbarton
removed
the
needs-documentation
|
I added a bunch of file documentation, in order to familiarize myself with the new documentation conventions. |
|
Also, LGTM code-wise. |
jcommelin
reviewed
Sep 3, 2019
jcommelin
approved these changes
Sep 3, 2019
jcommelin
added
the
ready-to-merge
anrddh
pushed a commit
to anrddh/mathlib
that referenced
this pull request
May 15, 2020
…egory_theory sense (leanprover-community#1259) * feat(measure_theory): prove that the Giry monad is a monad in the category_theory sense * Add spaces to fix alignment * document Measure * Add documentation * Add space before colon
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This is independent of #1258 and #1257.