mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily

Goal state before:
pp: I J : Finset ℝ≥0
hJI : J ⊆ I
this : Finset.restrict₂ hJI ∘ ⇑(MeasurableEquiv.toLp 2 (↥I → ℝ)).symm = ofLp ∘ ⇑(EuclideanSpace.restrict₂ hJI)
⊢ projectiveFamily J =
    Measure.map (Finset.restrict₂ hJI ∘ ⇑(MeasurableEquiv.toLp 2 (↥I → ℝ)).symm) (multivariateGaussian 0 (covMatrix I))

Tactic:
this,

Goal state after:
I J : Finset ℝ≥0
hJI : J ⊆ I
this : Finset.restrict₂ hJI ∘ ⇑(MeasurableEquiv.toLp 2 (↥I → ℝ)).symm = ofLp ∘ ⇑(EuclideanSpace.restrict₂ hJI)
⊢ projectiveFamily J = Measure.map (ofLp ∘ ⇑(EuclideanSpace.restrict₂ hJI)) (multivariateGaussian 0 (covMatrix I))
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: case hx.refine_2
E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
a : ℝ
inst✝ : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
ha_pos : 0 < a
c' : ℝ≥0∞
hc' : c' ≤ μ {x | ‖x‖ ≤ a}
hc'_gt : 2⁻¹ < c'
t : ℕ → ℝ := normThreshold a
c : ℝ≥0∞ := μ {x | ‖x‖ ≤ a}
C : ℝ := logRatio c' * a⁻¹ ^ 2
hc'_le : c' ≤ 1
ht_int_zero :
  ∫⁻ (x : E) in closedBall 0 a, ENNReal.ofReal (rexp (C * ‖x‖ ^ 2)) ∂μ ≤
    μ {x | ‖x‖ ≤ a} * ENNReal.ofReal (rexp (logRatio c'))
ha : ¬μ {x | ‖x‖ ≤ a} = 1
ha_lt : μ {x | ‖x‖ ≤ a} < 1
hc'_lt : c' < 1
h_iUnion : Set.univ = closedBall 0 a ∪ ⋃ n, closedBall 0 (t (n + 1)) \ closedBall 0 (t n)
this :
  ∫⁻ (x : E) in closedBall 0 (t 0) ∪ ⋃ n, closedBall 0 (t (n + 1)) \ closedBall 0 (t n),
      ENNReal.ofReal (rexp (C * ‖x‖ ^ 2)) ∂μ ≤
    ∫⁻ (x : E) in closedBall 0 (t 0), ENNReal.ofReal (rexp (C * ‖x‖ ^ 2)) ∂μ +
      ∑' (i : ℕ), ∫⁻ (x : E) in closedBall 0 (t (i + 1)) \ closedBall 0 (t i), ENNReal.ofReal (rexp (C * ‖x‖ ^ 2)) ∂μ
n : ℕ
⊢ 0 < 1 - c' ∧ 1 - c' < ∞

Tactic:
simp only [tsub_pos_iff_lt, hc'_lt, true_and]

Goal state after:
case hx.refine_2
E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
a : ℝ
inst✝ : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
ha_pos : 0 < a
c' : ℝ≥0∞
hc' : c' ≤ μ {x | ‖x‖ ≤ a}
hc'_gt : 2⁻¹ < c'
t : ℕ → ℝ := normThreshold a
c : ℝ≥0∞ := μ {x | ‖x‖ ≤ a}
C : ℝ := logRatio c' * a⁻¹ ^ 2
hc'_le : c' ≤ 1
ht_int_zero :
  ∫⁻ (x : E) in closedBall 0 a, ENNReal.ofReal (rexp (C * ‖x‖ ^ 2)) ∂μ ≤
    μ {x | ‖x‖ ≤ a} * ENNReal.ofReal (rexp (logRatio c'))
ha : ¬μ {x | ‖x‖ ≤ a} = 1
ha_lt : μ {x | ‖x‖ ≤ a} < 1
hc'_lt : c' < 1
h_iUnion : Set.univ = closedBall 0 a ∪ ⋃ n, closedBall 0 (t (n + 1)) \ closedBall 0 (t n)
this :
  ∫⁻ (x : E) in closedBall 0 (t 0) ∪ ⋃ n, closedBall 0 (t (n + 1)) \ closedBall 0 (t n),
      ENNReal.ofReal (rexp (C * ‖x‖ ^ 2)) ∂μ ≤
    ∫⁻ (x : E) in closedBall 0 (t 0), ENNReal.ofReal (rexp (C * ‖x‖ ^ 2)) ∂μ +
      ∑' (i : ℕ), ∫⁻ (x : E) in closedBall 0 (t (i + 1)) \ closedBall 0 (t i), ENNReal.ofReal (rexp (C * ‖x‖ ^ 2)) ∂μ
n : ℕ
⊢ 1 - c' < ∞
Module: Mathlib.Probability.Independence.Process.Basic

Goal state before:
pp: S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
α : Type u_4
mα : MeasurableSpace α
κ : Kernel α Ω
P : Measure α
𝓧 : S → Type u_5
𝓨 : Type u_6
inst✝² : (i : S) → MeasurableSpace (𝓧 i)
inst✝¹ : MeasurableSpace 𝓨
X : (i : S) → Ω → 𝓧 i
Y : Ω → 𝓨
hX : ∀ (i : S), Measurable (X i)
hY : Measurable Y
h : ∀ (I : Finset S), IndepFun (fun ω i ↦ X (↑i) ω) Y κ P
inst✝ : IsZeroOrMarkovKernel κ
πX : Set (Set Ω) := {s | ∃ t ∈ squareCylinders fun i ↦ {s | MeasurableSet s}, (fun ω i ↦ X i ω) ⁻¹' t = s}
πX_pi : IsPiSystem πX
πX_gen : MeasurableSpace.comap (fun ω i ↦ X i ω) MeasurableSpace.pi = generateFrom πX
I : Finset S
s : (i : S) → Set (𝓧 i)
t : Set 𝓨
ht : MeasurableSet t
hs : ∀ (i : S), MeasurableSet (s i)
this : (fun ω i ↦ X i ω) ⁻¹' (↑I).pi s = (fun ω i ↦ X (↑i) ω) ⁻¹' (↑Finset.univ).pi fun i ↦ s ↑i
h1 : MeasurableSet ((↑Finset.univ).pi fun i ↦ s ↑i)
ω : α
hω :
  (κ ω) (((fun ω i ↦ X (↑i) ω) ⁻¹' (↑Finset.univ).pi fun i ↦ s ↑i) ∩ Y ⁻¹' t) =
    (κ ω) ((fun ω i ↦ X (↑i) ω) ⁻¹' (↑Finset.univ).pi fun i ↦ s ↑i) * (κ ω) (Y ⁻¹' t)
⊢ (κ ω) ((fun ω i ↦ X i ω) ⁻¹' (↑I).pi s ∩ Y ⁻¹' t) = (κ ω) ((fun ω i ↦ X i ω) ⁻¹' (↑I).pi s) * (κ ω) (Y ⁻¹' t)

Tactic:
this,

Goal state after:
S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
α : Type u_4
mα : MeasurableSpace α
κ : Kernel α Ω
P : Measure α
𝓧 : S → Type u_5
𝓨 : Type u_6
inst✝² : (i : S) → MeasurableSpace (𝓧 i)
inst✝¹ : MeasurableSpace 𝓨
X : (i : S) → Ω → 𝓧 i
Y : Ω → 𝓨
hX : ∀ (i : S), Measurable (X i)
hY : Measurable Y
h : ∀ (I : Finset S), IndepFun (fun ω i ↦ X (↑i) ω) Y κ P
inst✝ : IsZeroOrMarkovKernel κ
πX : Set (Set Ω) := {s | ∃ t ∈ squareCylinders fun i ↦ {s | MeasurableSet s}, (fun ω i ↦ X i ω) ⁻¹' t = s}
πX_pi : IsPiSystem πX
πX_gen : MeasurableSpace.comap (fun ω i ↦ X i ω) MeasurableSpace.pi = generateFrom πX
I : Finset S
s : (i : S) → Set (𝓧 i)
t : Set 𝓨
ht : MeasurableSet t
hs : ∀ (i : S), MeasurableSet (s i)
this : (fun ω i ↦ X i ω) ⁻¹' (↑I).pi s = (fun ω i ↦ X (↑i) ω) ⁻¹' (↑Finset.univ).pi fun i ↦ s ↑i
h1 : MeasurableSet ((↑Finset.univ).pi fun i ↦ s ↑i)
ω : α
hω :
  (κ ω) (((fun ω i ↦ X (↑i) ω) ⁻¹' (↑Finset.univ).pi fun i ↦ s ↑i) ∩ Y ⁻¹' t) =
    (κ ω) ((fun ω i ↦ X (↑i) ω) ⁻¹' (↑Finset.univ).pi fun i ↦ s ↑i) * (κ ω) (Y ⁻¹' t)
⊢ (κ ω) (((fun ω i ↦ X (↑i) ω) ⁻¹' (↑Finset.univ).pi fun i ↦ s ↑i) ∩ Y ⁻¹' t) =
    (κ ω) ((fun ω i ↦ X (↑i) ω) ⁻¹' (↑Finset.univ).pi fun i ↦ s ↑i) * (κ ω) (Y ⁻¹' t)
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
a : ℝ
ha_pos : 0 < a
ha_gt : 2⁻¹ < μ {x | ‖x‖ ≤ a}
ha_lt : μ {x | ‖x‖ ≤ a} < 1
c : ℝ≥0∞ := μ {x | ‖x‖ ≤ a}
hc_lt : c < 1
hc_lt_top : c < ∞
hc_one_sub_lt_top : 1 - c < ∞
h_one_sub_lt_self : 1 - c < c
h_pos : 0 < logRatio c * a⁻¹ ^ 2
⊢ HasFiniteIntegral (fun x ↦ rexp (logRatio c * a⁻¹ ^ 2 * ‖x‖ ^ 2)) μ

Tactic:
simp only [HasFiniteIntegral, ← ofReal_norm, Real.norm_eq_abs, Real.abs_exp]

Goal state after:
E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
a : ℝ
ha_pos : 0 < a
ha_gt : 2⁻¹ < μ {x | ‖x‖ ≤ a}
ha_lt : μ {x | ‖x‖ ≤ a} < 1
c : ℝ≥0∞ := μ {x | ‖x‖ ≤ a}
hc_lt : c < 1
hc_lt_top : c < ∞
hc_one_sub_lt_top : 1 - c < ∞
h_one_sub_lt_self : 1 - c < c
h_pos : 0 < logRatio c * a⁻¹ ^ 2
⊢ ∫⁻ (a_1 : E), ENNReal.ofReal (rexp (logRatio c * a⁻¹ ^ 2 * ‖a_1‖ ^ 2)) ∂μ < ∞
Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess

Goal state before:
pp: T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁶ : LinearOrder T
inst✝⁵ : Bot T
R : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousAdd E
X : T → Ω → E
h : ∀ᵐ (ω : Ω) ∂P, X ⊥ ω = 0
I : Finset T
⊢ (fun ω ↦ I.restrict fun x ↦ X x ω) =ᵐ[P]
    ⇑(incrementsToRestrict R I) ∘ fun ω i ↦
      X (I.orderEmbOfFinWithBot i.succ) ω - X (I.orderEmbOfFinWithBot i.castSucc) ω

Tactic:
filter_upwards [h] with ω hω

Goal state after:
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁶ : LinearOrder T
inst✝⁵ : Bot T
R : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousAdd E
X : T → Ω → E
h : ∀ᵐ (ω : Ω) ∂P, X ⊥ ω = 0
I : Finset T
ω : Ω
hω : X ⊥ ω = 0
⊢ (I.restrict fun x ↦ X x ω) =
    (⇑(incrementsToRestrict R I) ∘ fun ω i ↦
        X (I.orderEmbOfFinWithBot i.succ) ω - X (I.orderEmbOfFinWithBot i.castSucc) ω)
      ω
Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess

Goal state before:
pp: T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁷ : LinearOrder T
inst✝⁶ : OrderBot T
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
inst✝ : CompleteSpace E
X : T → Ω → E
law : ∀ (t : T), HasGaussianLaw (X t) P
h_bot : ∀ᵐ (ω : Ω) ∂P, X ⊥ ω = 0
incr : HasIndepIncrements X P
I : Finset T
⊢ HasGaussianLaw (fun ω ↦ I.restrict fun x ↦ X x ω) P

Tactic:
by
    -- Label `t₁ < ... < tₙ` the elements of `I`.
    -- We want to show that `(X t₁, ..., X tₙ)` is Gaussian.
    have := (law ⊥).isProbabilityMeasure
    obtain rfl | hI := I.eq_empty_or_nonempty
    · -- If `I` is empty, there is nothing to say.
      exact .of_subsingleton
    -- Otherwise we know that `(X t₁, ..., X tₙ) = f (X t₁ - X ⊥, X t₂ - X t₁, ..., X tₙ - X tₙ₋₁)`
    -- almost surely (because `X ⊥ = 0` almost surely)
    -- for a certain continuous linear map `f` called here `incrementsToRestrict I`.
    have := incrementsToRestrict_increments_orderEmbOfFinWithBot_ae_eq_restrict ℝ h_bot I
    -- Therefore it is enough to show that `(X t₁ - X ⊥, X t₂ - X t₁, ..., X tₙ - X tₙ₋₁)` is
    -- Gaussian.
    refine .congr (.map ?_ _) this.symm
    -- Because they are independent, it is enough to show that each `X tᵢ₊₁ - X tᵢ` is Gaussian.
    refine (incr _ _ (monotone_orderEmbOfFinWithBot I)).hasGaussianLaw fun i ↦ ?_
    -- Because `X tᵢ` and `X tᵢ₊₁` are Gaussian, it is enough to show that
    -- `X tᵢ` is independent from `X tᵢ₊₁ - X tᵢ`.
    refine IndepFun.hasGaussianLaw_sub_of_sub (law _) (law _) ?_
    -- This follows from the fact that `X` has independent increments and `X ⊥ = 0` almost surely.
    exact incr.indepFun_eval_sub bot_le
      (monotone_orderEmbOfFinWithBot I (Fin.castSucc_le_succ i)) h_bot

Goal state after:
Module: Mathlib.Probability.Independence.Process.Basic

Goal state before:
pp: S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
α : Type u_4
mα : MeasurableSpace α
κ : Kernel α Ω
P : Measure α
T : S → Type u_5
𝓧 : (i : S) → T i → Type u_6
inst✝ : (i : S) → (j : T i) → MeasurableSpace (𝓧 i j)
X : (i : S) → (j : T i) → Ω → 𝓧 i j
hX : ∀ (i : S) (j : T i), Measurable (X i j)
h : ∀ (I : Finset S) (J : (i : ↥I) → Finset (T ↑i)), iIndepFun (fun i ω j ↦ X (↑i) (↑j) ω) κ P
hμ : P ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[P] ⇑η
hη✝ : IsMarkovKernel η
π : S → Set (Set Ω) := fun i ↦ {s | ∃ t ∈ squareCylinders fun j ↦ {s | MeasurableSet s}, (fun ω j ↦ X i j ω) ⁻¹' t = s}
π_pi : ∀ (i : S), IsPiSystem (π i)
π_gen : ∀ (i : S), MeasurableSpace.comap (fun ω j ↦ X i j ω) MeasurableSpace.pi = generateFrom (π i)
I : Finset S
s : S → Set Ω
J : (i : S) → Finset (T i)
t : (i : S) → (i_1 : T i) → Set (𝓧 i i_1)
ht : ∀ i ∈ I, ∀ (i_1 : T i), MeasurableSet (t i i_1)
hs : ∀ i ∈ I, (fun ω j ↦ X i j ω) ⁻¹' (↑(J i)).pi (t i) = s i
this :
  ⋂ i ∈ I, (fun ω j ↦ X i j ω) ⁻¹' (↑(J i)).pi (t i) =
    ⋂ i ∈ Finset.univ, (fun ω j ↦ X (↑i) (↑j) ω) ⁻¹' (↑Finset.univ).pi fun j ↦ t ↑i ↑j
h' : ∀ i ∈ Finset.univ, MeasurableSet ((↑Finset.univ).pi fun j ↦ t ↑i ↑j)
ω : α
hω :
  (κ ω) (⋂ i ∈ Finset.univ, (fun ω j ↦ X (↑i) (↑j) ω) ⁻¹' (↑Finset.univ).pi fun j ↦ t ↑i ↑j) =
    ∏ i, (κ ω) ((fun ω j ↦ X (↑i) (↑j) ω) ⁻¹' (↑Finset.univ).pi fun j ↦ t ↑i ↑j)
hη : κ ω = η ω
⊢ (η ω) (⋂ i ∈ I, (fun ω j ↦ X i j ω) ⁻¹' (↑(J i)).pi (t i)) =
    ∏ i ∈ I, (η ω) ((fun ω j ↦ X i j ω) ⁻¹' (↑(J i)).pi (t i))

Tactic:
this,

Goal state after:
S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
α : Type u_4
mα : MeasurableSpace α
κ : Kernel α Ω
P : Measure α
T : S → Type u_5
𝓧 : (i : S) → T i → Type u_6
inst✝ : (i : S) → (j : T i) → MeasurableSpace (𝓧 i j)
X : (i : S) → (j : T i) → Ω → 𝓧 i j
hX : ∀ (i : S) (j : T i), Measurable (X i j)
h : ∀ (I : Finset S) (J : (i : ↥I) → Finset (T ↑i)), iIndepFun (fun i ω j ↦ X (↑i) (↑j) ω) κ P
hμ : P ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[P] ⇑η
hη✝ : IsMarkovKernel η
π : S → Set (Set Ω) := fun i ↦ {s | ∃ t ∈ squareCylinders fun j ↦ {s | MeasurableSet s}, (fun ω j ↦ X i j ω) ⁻¹' t = s}
π_pi : ∀ (i : S), IsPiSystem (π i)
π_gen : ∀ (i : S), MeasurableSpace.comap (fun ω j ↦ X i j ω) MeasurableSpace.pi = generateFrom (π i)
I : Finset S
s : S → Set Ω
J : (i : S) → Finset (T i)
t : (i : S) → (i_1 : T i) → Set (𝓧 i i_1)
ht : ∀ i ∈ I, ∀ (i_1 : T i), MeasurableSet (t i i_1)
hs : ∀ i ∈ I, (fun ω j ↦ X i j ω) ⁻¹' (↑(J i)).pi (t i) = s i
this :
  ⋂ i ∈ I, (fun ω j ↦ X i j ω) ⁻¹' (↑(J i)).pi (t i) =
    ⋂ i ∈ Finset.univ, (fun ω j ↦ X (↑i) (↑j) ω) ⁻¹' (↑Finset.univ).pi fun j ↦ t ↑i ↑j
h' : ∀ i ∈ Finset.univ, MeasurableSet ((↑Finset.univ).pi fun j ↦ t ↑i ↑j)
ω : α
hω :
  (κ ω) (⋂ i ∈ Finset.univ, (fun ω j ↦ X (↑i) (↑j) ω) ⁻¹' (↑Finset.univ).pi fun j ↦ t ↑i ↑j) =
    ∏ i, (κ ω) ((fun ω j ↦ X (↑i) (↑j) ω) ⁻¹' (↑Finset.univ).pi fun j ↦ t ↑i ↑j)
hη : κ ω = η ω
⊢ (η ω) (⋂ i ∈ Finset.univ, (fun ω j ↦ X (↑i) (↑j) ω) ⁻¹' (↑Finset.univ).pi fun j ↦ t ↑i ↑j) =
    ∏ i ∈ I, (η ω) ((fun ω j ↦ X i j ω) ⁻¹' (↑(J i)).pi (t i))
Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes

Goal state before:
pp: t : ℚ
⊢ ⨅ r, defaultRatCDF ↑r = defaultRatCDF t

Tactic:
simp only [defaultRatCDF]
  have h_bdd : BddBelow (range fun r : ↥(Ioi t) ↦ ite ((r : ℚ) < 0) (0 : ℝ) 1) := by
    refine ⟨0, fun x hx ↦ ?_⟩
    obtain ⟨y, rfl⟩ := mem_range.mpr hx
    dsimp only
    split_ifs
    exacts [le_rfl, zero_le_one]
  split_ifs with h
  · refine le_antisymm ?_ (le_ciInf fun x ↦ ?_)
    · obtain ⟨q, htq, hq_neg⟩ : ∃ q, t < q ∧ q < 0 := ⟨t / 2, by linarith, by linarith⟩
      refine (ciInf_le h_bdd ⟨q, htq⟩).trans ?_
      rw [if_pos]
      rwa [Subtype.coe_mk]
    · split_ifs
      exacts [le_rfl, zero_le_one]
  · refine le_antisymm ?_ ?_
    · refine (ciInf_le h_bdd ⟨t + 1, lt_add_one t⟩).trans ?_
      split_ifs
      exacts [zero_le_one, le_rfl]
    · refine le_ciInf fun x ↦ ?_
      rw [if_neg]
      rw [not_lt] at h ⊢
      exact h.trans (mem_Ioi.mp x.prop).le

Goal state after:
Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes

Goal state before:
pp: α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
x : ℝ
⊢ Measurable fun a ↦ ↑(hf.stieltjesFunction a) x

Tactic:
have : (fun a ↦ hf.stieltjesFunction a x) = fun a ↦ ⨅ r : { r' : ℚ // x < r' }, f a ↑r := by
    ext1 a
    rw [← StieltjesFunction.iInf_rat_gt_eq]
    congr with q
    rw [stieltjesFunction_eq]
  rw [this]
  exact .iInf (fun q ↦ hf.measurable.eval)

Goal state after:
Module: Mathlib.Probability.Kernel.Disintegration.CondCDF

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
h_empty : ρ (s ×ˢ ∅) = 0
h_neg : Tendsto (fun r ↦ ρ (s ×ˢ Iic ↑(-r))) atTop (𝓝 (ρ (⋂ r, s ×ˢ Iic ↑r)))
h_inter_eq : ⋂ r, s ×ˢ Iic ↑(-r) = ⋂ r, s ×ˢ Iic ↑r
⊢ Tendsto (fun r ↦ ρ (s ×ˢ Iic ↑r)) atBot (𝓝 (ρ (⋂ i, s ×ˢ Iic ↑i)))

Tactic:
exact tendsto_comp_neg_atTop_iff.mp h_neg

Goal state after:
Module: Mathlib.Probability.Kernel.Disintegration.CondCDF

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
r : ℚ
s : Set α
hs : MeasurableSet s
inst✝ : IsFiniteMeasure ρ
this : ∀ (r : ℚ), ∫⁻ (x : α) in s, preCDF ρ r x ∂ρ.fst = ∫⁻ (x : α) in s, (preCDF ρ r * 1) x ∂ρ.fst
⊢ ∫⁻ (x : α) in s, preCDF ρ r x ∂ρ.fst = (ρ.IicSnd ↑r) s

Tactic:
this,

Goal state after:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
r : ℚ
s : Set α
hs : MeasurableSet s
inst✝ : IsFiniteMeasure ρ
this : ∀ (r : ℚ), ∫⁻ (x : α) in s, preCDF ρ r x ∂ρ.fst = ∫⁻ (x : α) in s, (preCDF ρ r * 1) x ∂ρ.fst
⊢ ∫⁻ (x : α) in s, (preCDF ρ r * 1) x ∂ρ.fst = (ρ.IicSnd ↑r) s
Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel

Goal state before:
pp: case refine_3
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝ : IsFiniteKernel ν
a : α
q : ℚ
t : β
hbdd_below : ∀ (q : ℚ), BddBelow (range fun r ↦ f (a, t) ↑r)
h_nonneg : ∀ (q : ℚ), 0 ≤ f (a, t) q
h_le_one : ∀ (q : ℚ), f (a, t) q ≤ 1
⊢ f (a, t) ↑⟨q + 1, ⋯⟩ ≤ 1

Tactic:
· exact h_le_one _

Goal state after:
Module: Mathlib.Probability.CentralLimitTheorem

Goal state before:
pp: case e'_12
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
P : Measure Ω
P' : Measure Ω'
X : ℕ → Ω → ℝ
Y : Ω' → ℝ
inst✝¹ : IsProbabilityMeasure P
inst✝ : IsProbabilityMeasure P'
hY : HasLaw Y (gaussianReal 0 Var[X 0; P].toNNReal) P'
hX : MemLp (X 0) 2 P
hindep : iIndepFun X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
h : Var[X 0; P] ≠ 0
this : HasLaw (fun ω ↦ Y ω / √Var[X 0; P]) (gaussianReal 0 1) P'
⊢ Y = (fun x ↦ √Var[X 0; P] * x) ∘ fun ω ↦ Y ω / √Var[X 0; P]

Tactic:
· ext
    simp [field] -- simp [field, hX] triggers the unused simp arguments linter
    field_simp [h]

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence

Goal state before:
pp: case hX
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
F : Type u_3
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : MeasurableSpace E
inst✝⁹ : CompleteSpace E
inst✝⁸ : BorelSpace E
inst✝⁷ : SecondCountableTopology E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : MeasurableSpace F
inst✝⁴ : CompleteSpace F
inst✝³ : BorelSpace F
inst✝² : SecondCountableTopology F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
X : Ω → E
Y : Ω → F
hXY : HasGaussianLaw (fun ω ↦ (X ω, Y ω)) P
h : ∀ (L₁ : StrongDual ℝ E) (L₂ : StrongDual ℝ F), cov[⇑L₁ ∘ X, ⇑L₂ ∘ Y; P] = 0
this✝ : IsProbabilityMeasure P
L : StrongDual ℝ (E × F)
this : (⇑L ∘ fun ω ↦ (X ω, Y ω)) = ⇑(L ∘SL inl ℝ E F) ∘ X + ⇑(L ∘SL inr ℝ E F) ∘ Y
⊢ MemLp (⇑(L ∘SL inl ℝ E F) ∘ X) 2 P

Tactic:
exact (hXY.fst.map _).memLp_two

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence

Goal state before:
pp: case h.hf
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : SecondCountableTopology E
X Y : Ω → E
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
h : X ⟂ᵢ[P] Y - X
this : IsProbabilityMeasure P
L : StrongDual ℝ E
⊢ Integrable (⇑L ∘ X) P

Tactic:
exact (hX.map L).integrable

Goal state after:
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
inst✝ : IsFiniteKernel κ
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : ⋂ i, seq i = ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
h0 : (ν a) (countablePartitionSet n x) = 0
⊢ Tendsto (fun m ↦ ((κ a) (countablePartitionSet n x ×ˢ seq m) / (ν a) (countablePartitionSet n x)).toReal) atTop
    (𝓝 ((κ a) (countablePartitionSet n x ×ˢ ∅) / (ν a) (countablePartitionSet n x)).toReal)

Tactic:
simp_rw [h0, ENNReal.toReal_div]

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
inst✝ : IsFiniteKernel κ
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : ⋂ i, seq i = ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
h0 : (ν a) (countablePartitionSet n x) = 0
⊢ Tendsto (fun m ↦ ((κ a) (countablePartitionSet n x ×ˢ seq m)).toReal / ENNReal.toReal 0) atTop
    (𝓝 (((κ a) (countablePartitionSet n x ×ˢ ∅)).toReal / ENNReal.toReal 0))
Module: Mathlib.Probability.Kernel.Disintegration.Unique

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝¹ : IsFiniteMeasure ρ
κ : Kernel α ℝ
inst✝ : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
huniv : ∀ᵐ (x : α) ∂ρ.fst, (κ x) univ = (ρ.condKernel x) univ
x : α
⊢ (κ x) univ = (ρ.condKernel x) univ →
    ∀ (t : Set ℝ), MeasurableSet t → (κ x) t = (ρ.condKernel x) t → (κ x) tᶜ = (ρ.condKernel x) tᶜ

Tactic:
hxuniv

Goal state after:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝¹ : IsFiniteMeasure ρ
κ : Kernel α ℝ
inst✝ : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
huniv : ∀ᵐ (x : α) ∂ρ.fst, (κ x) univ = (ρ.condKernel x) univ
x : α
hxuniv : (κ x) univ = (ρ.condKernel x) univ
⊢ ∀ (t : Set ℝ), MeasurableSet t → (κ x) t = (ρ.condKernel x) t → (κ x) tᶜ = (ρ.condKernel x) tᶜ
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
A : Set γ
hA : MeasurableSet A
this : ∫ (x : γ) in A, κ.density ν a x s ∂ν a = limsup (fun i ↦ ∫ (x : γ) in A, κ.densityProcess ν i a x s ∂ν a) atTop
⊢ ∫ (x : γ) in A, κ.density ν a x s ∂ν a = ∫ (x : γ) in A, κ.densityProcess ν n a x s ∂ν a

Tactic:
this,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
A : Set γ
hA : MeasurableSet A
this : ∫ (x : γ) in A, κ.density ν a x s ∂ν a = limsup (fun i ↦ ∫ (x : γ) in A, κ.densityProcess ν i a x s ∂ν a) atTop
⊢ limsup (fun i ↦ ∫ (x : γ) in A, κ.densityProcess ν i a x s ∂ν a) atTop =
    ∫ (x : γ) in A, κ.densityProcess ν n a x s ∂ν a
Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
κ : Kernel α (β × Ω)
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) ℝ
inst✝ : IsSFiniteKernel η
hη : (κ.map (Prod.map id (embeddingReal Ω))).fst ⊗ₖ η = κ.map (Prod.map id (embeddingReal Ω))
e : Ω → ℝ := embeddingReal Ω
he : MeasurableEmbedding (embeddingReal Ω) := measurableEmbedding_embeddingReal Ω
κ' : Kernel α (β × ℝ) := κ.map (Prod.map id e)
hη' : κ'.fst ⊗ₖ η = κ'
h_prod_embed : MeasurableEmbedding (Prod.map id e)
this : κ = κ'.comapRight h_prod_embed
| κ

Tactic:
this,

Goal state after:
α : Type u_1
β : Type u_2
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
κ : Kernel α (β × Ω)
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) ℝ
inst✝ : IsSFiniteKernel η
hη : (κ.map (Prod.map id (embeddingReal Ω))).fst ⊗ₖ η = κ.map (Prod.map id (embeddingReal Ω))
e : Ω → ℝ := embeddingReal Ω
he : MeasurableEmbedding (embeddingReal Ω) := measurableEmbedding_embeddingReal Ω
κ' : Kernel α (β × ℝ) := κ.map (Prod.map id e)
hη' : κ'.fst ⊗ₖ η = κ'
h_prod_embed : MeasurableEmbedding (Prod.map id e)
this : κ = κ'.comapRight h_prod_embed
| κ'.comapRight h_prod_embed