diff --git a/Exchangeability/DeFinetti/ViaL2/AlphaIicCE.lean b/Exchangeability/DeFinetti/ViaL2/AlphaIicCE.lean index bd42a164..16ac61ab 100644 --- a/Exchangeability/DeFinetti/ViaL2/AlphaIicCE.lean +++ b/Exchangeability/DeFinetti/ViaL2/AlphaIicCE.lean @@ -283,8 +283,7 @@ lemma alphaIicCE_right_continuous_at have hm_le : TailSigma.tailSigma X ≤ (inferInstance : MeasurableSpace Ω) := TailSigma.tailSigma_le X hX_meas haveI h_fact : Fact (TailSigma.tailSigma X ≤ (inferInstance : MeasurableSpace Ω)) := ⟨hm_le⟩ - haveI h_sf : SigmaFinite (μ.trim hm_le) := - Exchangeability.Probability.sigmaFinite_trim μ hm_le + haveI h_sf : SigmaFinite (μ.trim hm_le) := inferInstance -- Step 1: Get decreasing rational sequence u_n → t with u_n > t obtain ⟨u, u_anti, u_gt, u_tendsto⟩ := Real.exists_seq_rat_strictAnti_tendsto t diff --git a/Exchangeability/DeFinetti/ViaMartingale/FutureFiltration.lean b/Exchangeability/DeFinetti/ViaMartingale/FutureFiltration.lean index 4882e44f..04f39f9d 100644 --- a/Exchangeability/DeFinetti/ViaMartingale/FutureFiltration.lean +++ b/Exchangeability/DeFinetti/ViaMartingale/FutureFiltration.lean @@ -105,10 +105,8 @@ case requires manual construction of spanning sets and is a mathlib gap. -/ lemma sigmaFinite_trim_tailSigma {Ω α : Type*} {m₀ : MeasurableSpace Ω} [MeasurableSpace α] {μ : @Measure Ω m₀} [IsFiniteMeasure μ] (X : ℕ → Ω → α) (hX : ∀ n, Measurable (X n)) : - SigmaFinite (μ.trim (tailSigma_le X hX)) := by - classical - -- Use the infrastructure from CondExp.lean - exact Exchangeability.Probability.sigmaFinite_trim μ (tailSigma_le X hX) + SigmaFinite (μ.trim (tailSigma_le X hX)) := + inferInstance /-! ### Helper lemmas for futureFiltration properties -/ diff --git a/Exchangeability/Probability/CondExp.lean b/Exchangeability/Probability/CondExp.lean index ebd3f7f0..04a2e350 100644 --- a/Exchangeability/Probability/CondExp.lean +++ b/Exchangeability/Probability/CondExp.lean @@ -6,7 +6,6 @@ Authors: Cameron Freer import Exchangeability.Probability.CondExpBasic import Exchangeability.Probability.CondProb import Exchangeability.Probability.IntegrationHelpers -import ForMathlib.MeasureTheory.Measure.TrimInstances import Mathlib.Probability.Independence.Basic import Mathlib.Probability.Independence.Conditional import Mathlib.Probability.Martingale.Basic @@ -65,10 +64,6 @@ This file centralizes these patterns to keep the main proofs clean and maintaina - **Purpose**: Avoids typeclass metavariable issues in `μ[f | m]` - **Used in**: ViaMartingale finite-future sigma algebras -- **`sigmaFinite_trim`**: Trimmed measure is sigma-finite (when base is finite) - - **Used in**: ViaMartingale, multiple sub-σ-algebra constructions - - **Note**: `isFiniteMeasure_trim` is now in mathlib as an instance - ## Design Philosophy **Extract patterns that:** @@ -299,19 +294,6 @@ lemma condExp_indicator_mul_indicator_of_condIndep These wrappers provide explicit instance management for conditional expectations with sub-σ-algebras, working around Lean 4 typeclass inference issues. -/ -/-! ### SigmaFinite instances for trimmed measures - -When working with conditional expectations on sub-σ-algebras, we need `SigmaFinite (μ.trim hm)`. -For probability measures (or finite measures), this follows from showing the trimmed measure -is still finite. - -These lemmas are now in `ForMathlib.MeasureTheory.Measure.TrimInstances` and re-exported here -for backward compatibility. -/ - --- Re-export from ForMathlib for backward compatibility --- Note: isFiniteMeasure_trim is now in mathlib (as an instance), only sigmaFinite_trim is local -export MeasureTheory.Measure (sigmaFinite_trim) - /-! ### Stable conditional expectation wrapper This wrapper manages typeclass instances to avoid metavariable issues @@ -330,7 +312,7 @@ def condExpWith {Ω : Type*} {m₀ : MeasurableSpace Ω} classical haveI : IsFiniteMeasure μ := inferInstance -- IsFiniteMeasure (μ.trim _hm) is now automatic via mathlib instance - haveI : SigmaFinite (μ.trim _hm) := sigmaFinite_trim μ _hm + haveI : SigmaFinite (μ.trim _hm) := inferInstance exact μ[f | m] /-! ### Bridge lemma for indicator factorization @@ -356,7 +338,7 @@ lemma condexp_indicator_inter_bridge μ[B.indicator (fun _ => (1 : ℝ)) | m]) := by classical -- Install trimmed instances (IsFiniteMeasure is automatic via mathlib) - haveI : SigmaFinite (μ.trim hm) := sigmaFinite_trim μ hm + haveI : SigmaFinite (μ.trim hm) := inferInstance -- Forward to the proven lemma exact condExp_indicator_mul_indicator_of_condIndep hm hmF hmH hCI hA hB @@ -608,7 +590,7 @@ lemma condExp_mul_pullout {Ω : Type*} {m₀ : MeasurableSpace Ω} {μ : Measure have hg_bound : ∀ᵐ ω ∂μ, ‖g ω‖ ≤ C := ae_of_all μ fun ω => (Real.norm_eq_abs _).le.trans (hC ω) -- Provide typeclass instances explicitly (IsFiniteMeasure is automatic via mathlib) - haveI : SigmaFinite (μ.trim hm) := sigmaFinite_trim μ hm + haveI : SigmaFinite (μ.trim hm) := inferInstance -- Now condExp_stronglyMeasurable_mul_of_bound can resolve instances have h := condExp_stronglyMeasurable_mul_of_bound hm hg_strong hf C hg_bound diff --git a/Exchangeability/Probability/CondExpBasic.lean b/Exchangeability/Probability/CondExpBasic.lean index b69e103b..89a85b07 100644 --- a/Exchangeability/Probability/CondExpBasic.lean +++ b/Exchangeability/Probability/CondExpBasic.lean @@ -17,9 +17,6 @@ improve compilation speed. ## Main components -### σ-Finiteness -- `sigmaFinite_trim_of_le`: Trimmed measure inherits σ-finiteness from finite measures - ### Indicators - `indicator_iUnion_tsum_of_pairwise_disjoint`: Union of disjoint indicators equals their sum @@ -40,14 +37,6 @@ to work with multiple measurable space structures (e.g., for trimmed measures). section variable `[MeasurableSpace Ω]` unused for those lemmas, requiring `set_option linter.unusedSectionVars false`. -/ -set_option linter.unusedSectionVars false in -/-- If `μ` is finite, then any trim of `μ` is σ-finite. -/ -@[nolint unusedArguments] -lemma sigmaFinite_trim_of_le {m m₀ : MeasurableSpace Ω} - (μ : Measure Ω) [IsFiniteMeasure μ] (hm : m ≤ m₀) : - SigmaFinite (μ.trim hm) := - (inferInstance : IsFiniteMeasure (μ.trim hm)).toSigmaFinite - set_option linter.unusedSectionVars false in /-- For pairwise disjoint sets, the indicator of the union equals the pointwise `tsum` of indicators (for ℝ-valued constants). -/ diff --git a/Exchangeability/Probability/CondIndep/KallenbergIndicator.lean b/Exchangeability/Probability/CondIndep/KallenbergIndicator.lean index fda0cf0d..7d74ec2e 100644 --- a/Exchangeability/Probability/CondIndep/KallenbergIndicator.lean +++ b/Exchangeability/Probability/CondIndep/KallenbergIndicator.lean @@ -96,8 +96,9 @@ lemma condIndep_indicator_of_dropInfoY obtain ⟨S, hS_meas, rfl⟩ := hs exact hS_meas.preimage (hZ.prodMk hW) - -- SigmaFinite instance for trim (needed for condExp lemmas) - haveI hσZW : SigmaFinite (μ.trim hmZW_le) := sigmaFinite_trim_of_le μ hmZW_le + -- SigmaFinite instance for trim (needed for condExp lemmas); provided automatically + -- via mathlib's `isFiniteMeasure_trim` instance + `IsFiniteMeasure.toSigmaFinite`. + haveI hσZW : SigmaFinite (μ.trim hmZW_le) := inferInstance -- Integrability of indicators (bounded by 1) have hIndA_int : Integrable indA μ := (integrable_const 1).indicator (hA.preimage hY) diff --git a/ForMathlib.lean b/ForMathlib.lean deleted file mode 100644 index bfc017c7..00000000 --- a/ForMathlib.lean +++ /dev/null @@ -1 +0,0 @@ -import ForMathlib.MeasureTheory.Measure.TrimInstances diff --git a/ForMathlib/MeasureTheory/Measure/TrimInstances.lean b/ForMathlib/MeasureTheory/Measure/TrimInstances.lean deleted file mode 100644 index e8316b58..00000000 --- a/ForMathlib/MeasureTheory/Measure/TrimInstances.lean +++ /dev/null @@ -1,45 +0,0 @@ -/- -Copyright (c) 2025 Cameron Freer. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Cameron Freer --/ -import Mathlib.MeasureTheory.Measure.Trim - -/-! -# Sigma-Finiteness for Trimmed Measures - -This file provides a lemma showing that `μ.trim hm` is sigma-finite when `μ` is finite. - -## Main Results - -* `sigmaFinite_trim`: If `μ` is a finite measure, then `μ.trim hm` is sigma-finite. - -## Implementation Notes - -This lemma is useful when working with conditional expectations on sub-σ-algebras, -where mathlib's `condExp` requires `SigmaFinite (μ.trim hm)`. - -Note: `IsFiniteMeasure (μ.trim hm)` is now provided by mathlib as an instance -(`MeasureTheory.Measure.isFiniteMeasure_trim`), so we only need the sigma-finite corollary. - -## References - -* Kallenberg (2005), *Probabilistic Symmetries and Invariance Principles* --/ - -open MeasureTheory - -namespace MeasureTheory.Measure - -variable {Ω : Type*} {m₀ : MeasurableSpace Ω} - -/-- Trimmed measure is sigma-finite when the original measure is finite. - -This is the instance typically needed for `condExp` on sub-σ-algebras. -The finiteness of `μ.trim hm` is automatic via mathlib's `isFiniteMeasure_trim` instance. -/ -lemma sigmaFinite_trim (μ : Measure Ω) [IsFiniteMeasure μ] - {m : MeasurableSpace Ω} (hm : m ≤ m₀) : - SigmaFinite (μ.trim hm) := - inferInstance - -end MeasureTheory.Measure diff --git a/lakefile.toml b/lakefile.toml index eb7fb756..cb4d253b 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -1,6 +1,6 @@ name = "exchangeability" version = "0.1.0" -defaultTargets = ["Exchangeability", "ForMathlib"] +defaultTargets = ["Exchangeability"] [[require]] name = "mathlib" @@ -11,8 +11,5 @@ rev = "v4.30.0-rc2" name = "checkdecls" git = "https://github.com/PatrickMassot/checkdecls.git" -[[lean_lib]] -name = "ForMathlib" - [[lean_lib]] name = "Exchangeability"