fill sorries in 1) Prod and in 2) measurable_of_measurable_coe' adding IsPiSystem t #13
Conversation
- add additional hypothesis in toReal_ae_eq_indicator_condExp_iff_forall_meas_inter_eq that `g < ⊤` a.e
There was a problem hiding this comment.
Thanks for the PR! In the future, it's always good to discuss your plans on Zulip first, but here you got lucky and nobody was working on that. I personally find the possibility of GibbsMeasure being used in PhysLean very exciting!
Here are a few initial comments. Your PR is coming at a very busy time for me, so I will likely not be able to comment further before another month. However, more or less all of your code could go straight into mathlib, so I would encourage you to PR it there, where there will be reviewers available for you. No need to close this PR, at least for now.
GibbsMeasure/Mathlib/MeasureTheory/Function/ConditionalExpectation/Basic.lean
Outdated
Show resolved
Hide resolved
| lemma measure_univ_of_marg_snd_dirac | ||
| (μ : Measure (X × Y)) (y : Y) | ||
| (marg_Y : Measure.map Prod.snd μ = Measure.dirac y) : | ||
| μ univ = 1 := by |
There was a problem hiding this comment.
Is this really a theorem about product and Dirac measures? It seems to me like you can state everything in the generality of HasLaw
|
Thank you very much for your review. I'm going to have another take on them soon and will try to PR them to mathlib. Next time will use the GibbsMeasure zulip channel :) |
YaelDillies
added
the
awaiting-author
|
oh sorry, I have just seen your comments :), will try to address them now. Thanks |
|
-awaiting-author |
YaelDillies
removed
the
awaiting-author
| @@ -1,17 +1,349 @@ | |||
| import Mathlib.MeasureTheory.Measure.Prod | |||
| import Mathlib.Probability.HasLaw | |||
There was a problem hiding this comment.
Mathlib.Probability.HasLaw imports Mathlib.MeasureTheory.Measure.Prod, not the other way around. Therefore all your material that depends on HasLaw should go to GibbsMeasure.Mathlib.Probability.HasLaw instead of GibbsMeasure.Mathlib.MeasureTheory.Measure.Prod
| [SigmaFinite (μ.trim hm)] {g : α → ℝ≥0∞} {s : Set α} | ||
| (hs_meas : MeasurableSet s) (hs_finite : μ s ≠ ⊤) | ||
| (hgm : AEStronglyMeasurable[m] g μ) | ||
| (hg_fin : ∀ᵐ a ∂ μ, g a ≠ ⊤) : | ||
| (fun a ↦ (g a).toReal) =ᵐ[μ] μ[s.indicator 1| m] ↔ | ||
| ∀ t, MeasurableSet[m] t → μ (s ∩ t) = ∫⁻ a in t, g a ∂μ := by |
There was a problem hiding this comment.
Statement is indented by four spaces
| [SigmaFinite (μ.trim hm)] {g : α → ℝ≥0∞} {s : Set α} | |
| (hs_meas : MeasurableSet s) (hs_finite : μ s ≠ ⊤) | |
| (hgm : AEStronglyMeasurable[m] g μ) | |
| (hg_fin : ∀ᵐ a ∂ μ, g a ≠ ⊤) : | |
| (fun a ↦ (g a).toReal) =ᵐ[μ] μ[s.indicator 1| m] ↔ | |
| ∀ t, MeasurableSet[m] t → μ (s ∩ t) = ∫⁻ a in t, g a ∂μ := by | |
| [SigmaFinite (μ.trim hm)] {g : α → ℝ≥0∞} {s : Set α} | |
| (hs_meas : MeasurableSet s) (hs_finite : μ s ≠ ⊤) | |
| (hgm : AEStronglyMeasurable[m] g μ) | |
| (hg_fin : ∀ᵐ a ∂ μ, g a ≠ ⊤) : | |
| (fun a ↦ (g a).toReal) =ᵐ[μ] μ[s.indicator 1| m] ↔ | |
| ∀ t, MeasurableSet[m] t → μ (s ∩ t) = ∫⁻ a in t, g a ∂μ := by |
Same everywhere else
| MeasureTheory.Measure.eq_mapMk_of_marg_fst_dirac (μ := μ) (x := x) (marg_X := margX) | ||
| simpa [μ, margY', hY.map_eq] using hμ | ||
| end | ||
| section |
There was a problem hiding this comment.
| section | |
| section |
YaelDillies
added
the
awaiting-author
3 participants
hope it is not impolite to work on this; apologies but I'd like to use GibbsMeasure in a few applications in PhysLean :)