mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case coe.inl
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁸ : Nonempty ι
u : ι → Ω → β
τ : Ω → WithTop ι
inst✝⁷ : LinearOrder ι
inst✝⁶ : MeasurableSpace ι
inst✝⁵ : TopologicalSpace ι
inst✝⁴ : OrderTopology ι
inst✝³ : SecondCountableTopology ι
inst✝² : BorelSpace ι
inst✝¹ : TopologicalSpace β
f : Filtration ι m
inst✝ : PseudoMetrizableSpace ι
h : IsStronglyProgressive f u
hτ : IsStoppingTime f τ
h_meas : IsStronglyProgressive f fun i ω ↦ (min (↑i) (τ ω)).untopA
i : ι
ω : Ω
t : ι
h_it : i ≤ t
⊢ (min ↑i ↑t).untopA ≤ i

Tactic:
simp [(mod_cast h_it : (i : WithTop ι) ≤ t)]

Goal state after:
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹⁰ : Nonempty ι
u : ι → Ω → β
τ : Ω → WithTop ι
inst✝⁹ : LinearOrder ι
inst✝⁸ : MeasurableSpace ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : OrderTopology ι
inst✝⁵ : SecondCountableTopology ι
inst✝⁴ : BorelSpace ι
inst✝³ : TopologicalSpace β
f : Filtration ι m
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
hf_prog : IsStronglyProgressive f u
hτ : IsStoppingTime f τ
h_str_meas : ∀ (i : ι), StronglyMeasurable (stoppedValue u fun ω ↦ min (τ ω) ↑i)
t : Set β
ht : MeasurableSet t
seq : ℕ → ι
h_seq_tendsto : Tendsto seq atTop atTop
⊢ MeasurableSet (stoppedValue u τ ⁻¹' t)

Tactic:
have : stoppedValue u τ ⁻¹' t
      = (⋃ n, stoppedValue u τ ⁻¹' t ∩ {ω | τ ω ≤ seq n})
        ∪ (stoppedValue u τ ⁻¹' t ∩ {ω | τ ω = ⊤}) := by
    ext1 ω
    simp only [Set.mem_preimage, Set.mem_union, Set.mem_iUnion, Set.mem_inter_iff,
      Set.mem_ofPred_eq, exists_and_left]
    rw [← and_or_left, iff_self_and]
    intro _
    by_cases h : τ ω = ⊤
    · exact .inr h
    · lift τ ω to ι using h with t
      simp only [coe_le_coe, coe_ne_top, or_false]
      rw [tendsto_atTop] at h_seq_tendsto
      exact (h_seq_tendsto t).exists

Goal state after:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹⁰ : Nonempty ι
u : ι → Ω → β
τ : Ω → WithTop ι
inst✝⁹ : LinearOrder ι
inst✝⁸ : MeasurableSpace ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : OrderTopology ι
inst✝⁵ : SecondCountableTopology ι
inst✝⁴ : BorelSpace ι
inst✝³ : TopologicalSpace β
f : Filtration ι m
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
hf_prog : IsStronglyProgressive f u
hτ : IsStoppingTime f τ
h_str_meas : ∀ (i : ι), StronglyMeasurable (stoppedValue u fun ω ↦ min (τ ω) ↑i)
t : Set β
ht : MeasurableSet t
seq : ℕ → ι
h_seq_tendsto : Tendsto seq atTop atTop
this :
  stoppedValue u τ ⁻¹' t = (⋃ n, stoppedValue u τ ⁻¹' t ∩ {ω | τ ω ≤ ↑(seq n)}) ∪ stoppedValue u τ ⁻¹' t ∩ {ω | τ ω = ⊤}
⊢ MeasurableSet (stoppedValue u τ ⁻¹' t)
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝² : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝¹ : PartialOrder ι
ℱ : Filtration ι m
inst✝ : NormedAddCommGroup E
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), Integrable (u n) μ
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω ∈ WithTop.some '' ↑s
⊢ Integrable (stoppedValue u τ) μ

Tactic:
by
  simp_rw [← memLp_one_iff_integrable] at hu ⊢
  exact memLp_stoppedValue_of_mem_finset hτ hu hbdd

Goal state after:
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: case pos
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace E
inst✝¹ : CompleteSpace F
inst✝ : MeasurableSpace E
μ : Measure E
L : E ≃L[𝕜] F
h : Integrable (fun x ↦ x) μ
⊢ ∫ (x : E), L x ∂μ = L (∫ (x : E), id x ∂μ)

pp: case neg
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace E
inst✝¹ : CompleteSpace F
inst✝ : MeasurableSpace E
μ : Measure E
L : E ≃L[𝕜] F
h : ¬Integrable (fun x ↦ x) μ
⊢ ∫ (x : E), L x ∂μ = L (∫ (x : E), id x ∂μ)

Tactic:
· exact ContinuousLinearMap.integral_comp_id_comm' h L.toContinuousLinearMap

Goal state after:
case neg
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace E
inst✝¹ : CompleteSpace F
inst✝ : MeasurableSpace E
μ : Measure E
L : E ≃L[𝕜] F
h : ¬Integrable (fun x ↦ x) μ
⊢ ∫ (x : E), L x ∂μ = L (∫ (x : E), id x ∂μ)
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: x t p : ℝ
hp : 0 ≤ p
ht : 0 < t
hp_zero : ¬p = 0
h_x_le : ∀ (c : ℝ), 0 < c → x ≤ c⁻¹ * rexp (c * x)
h_neg_x_le : ∀ (c : ℝ), 0 < c → -x ≤ c⁻¹ * rexp (-c * x)
h_abs_le : ∀ (c : ℝ), 0 < c → |x| ≤ c⁻¹ * max (rexp (c * x)) (rexp (-c * x))
⊢ -t / p = -(t / p)

Tactic:
rw [neg_div]

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
c : ℝ
hc : c ≠ 0
x : ℝ
⊢ (√↑v)⁻¹ * (√(2 * π))⁻¹ * rexp (-(c⁻¹ * x - μ) ^ 2 / (2 * ↑v)) =
    |c| * (√(2 * π * (c ^ 2 * ↑v)))⁻¹ * rexp (-(x - c * μ) ^ 2 / (2 * (c ^ 2 * ↑v)))

Tactic:
refine congr_arg₂ _ ?_ ?_

Goal state after:
case refine_1
μ : ℝ
v : ℝ≥0
c : ℝ
hc : c ≠ 0
x : ℝ
⊢ (√↑v)⁻¹ * (√(2 * π))⁻¹ = |c| * (√(2 * π * (c ^ 2 * ↑v)))⁻¹

case refine_2
μ : ℝ
v : ℝ≥0
c : ℝ
hc : c ≠ 0
x : ℝ
⊢ rexp (-(c⁻¹ * x - μ) ^ 2 / (2 * ↑v)) = rexp (-(x - c * μ) ^ 2 / (2 * (c ^ 2 * ↑v)))
Module: Mathlib.Probability.Distributions.Gaussian.Basic

Goal state before:
pp: m : ℝ
v : ℝ≥0
L : StrongDual ℝ ℝ
⊢ Measure.map (⇑L) (gaussianReal m v) =
    gaussianReal (∫ (x : ℝ), L x ∂gaussianReal m v) Var[⇑L; gaussianReal m v].toNNReal

Tactic:
rw [gaussianReal_map_continuousLinearMap]

Goal state after:
m : ℝ
v : ℝ≥0
L : StrongDual ℝ ℝ
⊢ gaussianReal (L m) ((L 1 ^ 2).toNNReal * v) =
    gaussianReal (∫ (x : ℝ), L x ∂gaussianReal m v) Var[⇑L; gaussianReal m v].toNNReal
Module: Mathlib.Probability.Moments.MGFAnalytic

Goal state before:
pp: case e'_2.e'_6
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst✝ : IsZeroOrProbabilityMeasure μ
ht : 0 < t
hc : ∫ (x : Ω), X x ∂μ = 0
hs : Set.Icc 0 t ⊆ interior (integrableExpSet X μ)
hu : UniqueDiffOn ℝ (Set.Icc 0 t)
x✝ : ℝ
⊢ 0 = taylorWithinEval (cgf X μ) 1 (Set.uIcc 0 t) 0 t

Tactic:
have hd : derivWithin (cgf X μ) (Set.Icc 0 t) 0 = 0 := by
      convert! (analyticAt_cgf (hs ⟨le_refl 0, le_of_lt ht⟩)).differentiableAt.derivWithin _
      · simpa [hc] using (deriv_cgf_zero (hs ⟨le_refl 0, le_of_lt ht⟩)).symm
      · exact hu 0 ⟨le_refl 0, le_of_lt ht⟩
    simp [hd, Set.uIcc_of_lt ht]

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
⊢ deriv (mgf (fun x ↦ x) (gaussianReal μ v)) 0 = μ

Tactic:
mgf_fun_id_gaussianReal,

Goal state after:
μ : ℝ
v : ℝ≥0
⊢ deriv (fun t ↦ rexp (μ * t + ↑v * t ^ 2 / 2)) 0 = μ
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
⊢ iteratedDeriv 2 (mgf (fun x ↦ x) (gaussianReal 0 v)) 0 = ↑v

Tactic:
mgf_fun_id_gaussianReal,

Goal state after:
μ : ℝ
v : ℝ≥0
⊢ iteratedDeriv 2 (fun t ↦ rexp (0 * t + ↑v * t ^ 2 / 2)) 0 = ↑v
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: m₁ m₂ : ℝ
v₁ v₂ : ℝ≥0
⊢ gaussianReal m₁ v₁ ∗ gaussianReal m₂ v₂ = gaussianReal (m₁ + m₂) (v₁ + v₂)

Tactic:
refine Measure.ext_of_charFun ?_
  ext t
  simp_rw [charFun_conv, charFun_gaussianReal]
  rw [← Complex.exp_add]
  simp only [Complex.ofReal_add, NNReal.coe_add]
  ring_nf

Goal state after:
Module: Mathlib.Probability.Moments.CovarianceBilin

Goal state before:
pp: ι : Type u_2
Ω : Type u_3
inst✝¹ : Fintype ι
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : ι → Ω → ℝ
hX : ∀ (i : ι), MemLp (X i) 2 μ
i j : ι
⊢ ((covarianceBilin (Measure.map (fun ω ↦ toLp 2 fun x ↦ X x ω) μ)) ((basisFun ι ℝ) i)) ((basisFun ι ℝ) j) =
    cov[X i, X j; μ]

Tactic:
by
  have (i : ι) := (hX i).aemeasurable
  rw [covarianceBilin_apply_eq_cov, covariance_map]
  · simp [basisFun_inner]; rfl
  · exact Measurable.aestronglyMeasurable (by fun_prop)
  · exact Measurable.aestronglyMeasurable (by fun_prop)
  · fun_prop
  · exact (memLp_map_measure_iff aestronglyMeasurable_id (by fun_prop)).2 (MemLp.of_eval_piLp hX)

Goal state after:
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: case hd
c d : ℝ≥0∞
hc : 2⁻¹ < c
hd : d < 1
h : c ≤ d
⊢ 0 < (1 - d).toReal

pp: case hb
c d : ℝ≥0∞
hc : 2⁻¹ < c
hd : d < 1
h : c ≤ d
⊢ d ≠ ∞

pp: case hb
c d : ℝ≥0∞
hc : 2⁻¹ < c
hd : d < 1
h : c ≤ d
⊢ 1 - c ≠ ∞

Tactic:
· simp only [ENNReal.toReal_pos_iff, tsub_pos_iff_lt, hd, true_and]
    finiteness

Goal state after:
case hb
c d : ℝ≥0∞
hc : 2⁻¹ < c
hd : d < 1
h : c ≤ d
⊢ d ≠ ∞

case hb
c d : ℝ≥0∞
hc : 2⁻¹ < c
hd : d < 1
h : c ≤ d
⊢ 1 - c ≠ ∞
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
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'
⊢ ∫⁻ (x : E), ENNReal.ofReal (rexp (logRatio c' * a⁻¹ ^ 2 * ‖x‖ ^ 2)) ∂μ ≤
    μ {x | ‖x‖ ≤ a} *
      (ENNReal.ofReal (rexp (logRatio c')) +
        ∑' (n : ℕ), ENNReal.ofReal (rexp (-2⁻¹ * Real.log (c' / (1 - c')).toReal * 2 ^ n)))

Tactic:
let t := normThreshold a

Goal state after:
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
⊢ ∫⁻ (x : E), ENNReal.ofReal (rexp (logRatio c' * a⁻¹ ^ 2 * ‖x‖ ^ 2)) ∂μ ≤
    μ {x | ‖x‖ ≤ a} *
      (ENNReal.ofReal (rexp (logRatio c')) +
        ∑' (n : ℕ), ENNReal.ofReal (rexp (-2⁻¹ * Real.log (c' / (1 - c')).toReal * 2 ^ n)))
Module: Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily

Goal state before:
pp: I✝ J I : Finset ℝ≥0
⊢ IsGaussian (projectiveFamily I)

Tactic:
rw [projectiveFamily,
    show ⇑(MeasurableEquiv.toLp 2 (I → ℝ)).symm = ⇑(EuclideanSpace.equiv I ℝ) from rfl]
  infer_instance

Goal state after:
Module: Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily

Goal state before:
pp: I : Finset ℝ≥0
s : ↥I
⊢ gaussianReal (∫ (x : ↥I → ℝ), x s ∂projectiveFamily I) Var[fun x ↦ x s; projectiveFamily I].toNNReal =
    gaussianReal 0 ↑s

Tactic:
integral_eval_projectiveFamily,

Goal state after:
I : Finset ℝ≥0
s : ↥I
⊢ gaussianReal 0 Var[fun x ↦ x s; projectiveFamily I].toNNReal = gaussianReal 0 ↑s
Module: Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily

Goal state before:
pp: case hf
I : Finset ℝ≥0
s t : ↥I
⊢ Integrable (fun x ↦ x s) (projectiveFamily I)

pp: case hg
I : Finset ℝ≥0
s t : ↥I
⊢ Integrable (fun x ↦ x t) (projectiveFamily I)

pp: case hX
I : Finset ℝ≥0
s t : ↥I
⊢ MemLp (fun x ↦ x s) 2 (projectiveFamily I)

pp: case hY
I : Finset ℝ≥0
s t : ↥I
⊢ MemLp (fun x ↦ x t) 2 (projectiveFamily I)

pp: I : Finset ℝ≥0
s t : ↥I
⊢ HasGaussianLaw (fun x ↦ x s - x t) (projectiveFamily I)

Tactic:
· exact (IsGaussian.hasGaussianLaw_id.eval s).integrable

Goal state after:
case hg
I : Finset ℝ≥0
s t : ↥I
⊢ Integrable (fun x ↦ x t) (projectiveFamily I)

case hX
I : Finset ℝ≥0
s t : ↥I
⊢ MemLp (fun x ↦ x s) 2 (projectiveFamily I)

case hY
I : Finset ℝ≥0
s t : ↥I
⊢ MemLp (fun x ↦ x t) 2 (projectiveFamily I)

I : Finset ℝ≥0
s t : ↥I
⊢ HasGaussianLaw (fun x ↦ x s - x t) (projectiveFamily I)
Module: Mathlib.Probability.Independence.CharacteristicFunction

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁴ : IsFiniteMeasure P
E : Type u_2
mE : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
X : Ω → E
inst✝ : NormedSpace ℝ E
Y : Ω → E
mX : AEMeasurable X P
mY : AEMeasurable Y P
hXY : X ⟂ᵢ[P] Y
L : StrongDual ℝ E
⊢ charFunDual (Measure.map X P ∗ Measure.map Y P) L = (charFunDual (Measure.map X P) * charFunDual (Measure.map Y P)) L

Tactic:
charFunDual_conv,

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁴ : IsFiniteMeasure P
E : Type u_2
mE : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
X : Ω → E
inst✝ : NormedSpace ℝ E
Y : Ω → E
mX : AEMeasurable X P
mY : AEMeasurable Y P
hXY : X ⟂ᵢ[P] Y
L : StrongDual ℝ E
⊢ charFunDual (Measure.map X P) L * charFunDual (Measure.map Y P) L =
    (charFunDual (Measure.map X P) * charFunDual (Measure.map Y P)) L
Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic

Goal state before:
pp: T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst✝⁴ : NormedAddCommGroup E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : SecondCountableTopology E
hX : IsGaussianProcess X P
I : Finset T
⊢ HasGaussianLaw (fun ω ↦ ∑ i ∈ I, X i ω) P

Tactic:
convert! hX.hasGaussianLaw_sum (I := I)
  simp

Goal state after:
Module: Mathlib.Probability.Independence.CharacteristicFunction

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
s : Finset ι
E : Type u_3
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
X : ι → Ω → E
inst✝ : NormedSpace ℝ E
mX : ∀ i ∈ s, AEMeasurable (X i) P
hX : iIndepFun (s.restrict X) P
⊢ charFunDual (Measure.map (fun ω ↦ ∑ i ∈ s, X i ω) P) = ∏ i ∈ s, charFunDual (Measure.map (X i) P)

Tactic:
convert! hX.charFunDual_map_finsetSum_eq_prod mX

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
s : Finset ι
E : Type u_3
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
X : ι → Ω → E
inst✝ : NormedSpace ℝ E
mX : ∀ i ∈ s, AEMeasurable (X i) P
hX : iIndepFun (s.restrict X) P
x✝ : Ω
⊢ ∑ i ∈ s, X i x✝ = (∑ i ∈ s, X i) x✝
Module: Mathlib.Probability.BrownianMotion.Basic

Goal state before:
pp: case e'_3
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
s t : ℝ≥0
⊢ ↑(min s t) = cov[Function.eval ⟨s, ⋯⟩, fun x ↦ x ⟨t, ⋯⟩; projectiveFamily {s, t}]

pp: case convert_1
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
s t : ℝ≥0
⊢ AEMeasurable (Function.eval ⟨s, ⋯⟩) (projectiveFamily {s, t})

pp: case convert_2
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
s t : ℝ≥0
⊢ AEMeasurable (fun x ↦ x ⟨t, ⋯⟩) (projectiveFamily {s, t})

Tactic:
· rw [covariance_eval_projectiveFamily]

Goal state after:
case convert_1
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
s t : ℝ≥0
⊢ AEMeasurable (Function.eval ⟨s, ⋯⟩) (projectiveFamily {s, t})

case convert_2
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
s t : ℝ≥0
⊢ AEMeasurable (fun x ↦ x ⟨t, ⋯⟩) (projectiveFamily {s, t})
Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes

Goal state before:
pp: α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
⊢ Tendsto (↑(hf.stieltjesFunction a)) atBot (𝓝 0)

Tactic:
by
  have h_exists : ∀ x : ℝ, ∃ q : ℚ, x < q ∧ ↑q < x + 1 := fun x ↦ exists_rat_btwn (lt_add_one x)
  let qs : ℝ → ℚ := fun x ↦ (h_exists x).choose
  have hqs_tendsto : Tendsto qs atBot atBot := by
    rw [tendsto_atBot_atBot]
    refine fun q ↦ ⟨q - 1, fun y hy ↦ ?_⟩
    have h_le : ↑(qs y) ≤ (q : ℝ) - 1 + 1 :=
      (h_exists y).choose_spec.2.le.trans (add_le_add hy le_rfl)
    rw [sub_add_cancel] at h_le
    exact mod_cast h_le
  refine tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds
    ((hf.tendsto_atBot_zero a).comp hqs_tendsto) (stieltjesFunction_nonneg hf a) fun x ↦ ?_
  rw [Function.comp_apply, ← stieltjesFunction_eq hf]
  exact (hf.stieltjesFunction a).mono (h_exists x).choose_spec.1.le

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst✝ : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
t : β
⊢ 0 ≤ ↑(stieltjesOfMeasurableRat f ⋯ (a, t)) x

Tactic:
exact stieltjesOfMeasurableRat_nonneg _ _ _

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
r : ℚ
inst✝ : IsFiniteMeasure ρ
⊢ ∫⁻ (x : α) in univ, preCDF ρ r x ∂ρ.fst = (ρ.IicSnd ↑r) univ

Tactic:
setLIntegral_preCDF_fst ρ r MeasurableSet.univ

Goal state after:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
r : ℚ
inst✝ : IsFiniteMeasure ρ
⊢ (ρ.IicSnd ↑r) univ = (ρ.IicSnd ↑r) univ
Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence

Goal state before:
pp: Ω : 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
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
hXY : X ⟂ᵢ[P] Y
this✝ : IsProbabilityMeasure P
L : StrongDual ℝ (E × F)
this :
  (∫ (x : E), x ∂Measure.map X P, ∫ (y : F), y ∂Measure.map Y P) =
    (inl ℝ E F) (∫ (x : E), x ∂Measure.map X P) + (inr ℝ E F) (∫ (y : F), y ∂Measure.map Y P)
⊢ charFunDual (Measure.map X P) (L ∘SL inl ℝ E F) * charFunDual (Measure.map Y P) (L ∘SL inr ℝ E F) =
    cexp
      (↑(L (∫ (x : E), x ∂Measure.map X P, ∫ (y : F), y ∂Measure.map Y P)) * I -
        ↑((((covarianceBilinDual (Measure.map X P)).diagonalStrongDualProd (covarianceBilinDual (Measure.map Y P))) L)
              L) /
          2)

Tactic:
simp only [this, map_add, ofReal_add, add_mul, diagonalStrongDualProd_apply, add_div,
      add_sub_add_comm, exp_add]

Goal state after:
Ω : 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
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
hXY : X ⟂ᵢ[P] Y
this✝ : IsProbabilityMeasure P
L : StrongDual ℝ (E × F)
this :
  (∫ (x : E), x ∂Measure.map X P, ∫ (y : F), y ∂Measure.map Y P) =
    (inl ℝ E F) (∫ (x : E), x ∂Measure.map X P) + (inr ℝ E F) (∫ (y : F), y ∂Measure.map Y P)
⊢ charFunDual (Measure.map X P) (L ∘SL inl ℝ E F) * charFunDual (Measure.map Y P) (L ∘SL inr ℝ E F) =
    cexp
        (↑(L ((inl ℝ E F) (∫ (x : E), x ∂Measure.map X P))) * I -
          ↑(((covarianceBilinDual (Measure.map X P)) (L ∘SL inl ℝ E F)) (L ∘SL inl ℝ E F)) / 2) *
      cexp
        (↑(L ((inr ℝ E F) (∫ (y : F), y ∂Measure.map Y P))) * I -
          ↑(((covarianceBilinDual (Measure.map Y P)) (L ∘SL inr ℝ E F)) (L ∘SL inr ℝ E F)) / 2)
Module: Mathlib.Probability.CentralLimitTheorem

Goal state before:
pp: Ω : 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 1) P'
h0 : ∫ (x : Ω), X 0 x ∂P = 0
h1 : ∫ (x : Ω), (X 0 ^ 2) x ∂P = 1
hindep : iIndepFun X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
⊢ Tendsto (fun n ↦ ⟨Measure.map (fun ω ↦ (√↑n)⁻¹ * ∑ k ∈ Finset.range n, X k ω) P, ⋯⟩) atTop (𝓝 ⟨Measure.map Y P', ⋯⟩)

Tactic:
refine ProbabilityMeasure.tendsto_iff_tendsto_charFun.2 fun t ↦ ?_

Goal state after:
Ω : 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 1) P'
h0 : ∫ (x : Ω), X 0 x ∂P = 0
h1 : ∫ (x : Ω), (X 0 ^ 2) x ∂P = 1
hindep : iIndepFun X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
t : ℝ
⊢ Tendsto (fun n ↦ charFun (↑⟨Measure.map (fun ω ↦ (√↑n)⁻¹ * ∑ k ∈ Finset.range n, X k ω) P, ⋯⟩) t) atTop
    (𝓝 (charFun (↑⟨Measure.map Y P', ⋯⟩) t))
Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence

Goal state before:
pp: case e_a.h
Ω : 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
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
hXY : X ⟂ᵢ[P] Y
this✝ : IsProbabilityMeasure P
L : StrongDual ℝ (E × F)
this :
  (∫ (x : E), x ∂Measure.map X P, ∫ (y : F), y ∂Measure.map Y P) =
    (inl ℝ E F) (∫ (x : E), x ∂Measure.map X P) + (inr ℝ E F) (∫ (y : F), y ∂Measure.map Y P)
⊢ MemLp id 2 (Measure.map Y P)

Tactic:
exact hY.isGaussian_map.memLp_two_id

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set β
hs : MeasurableSet s
t✝ t : Set ℝ
ht : MeasurableSet t
iht : ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f hf) (a, b)) t ∂ν a = (κ a) (s ×ˢ t)
⊢ (κ a) (s ×ˢ univ) - (κ a) (s ×ˢ t) = (κ a) (s ×ˢ tᶜ)

Tactic:
rw [← measure_sdiff _ (hs.prod ht).nullMeasurableSet (measure_ne_top _ _)]
        · rw [prod_sdiff_prod, compl_eq_univ_sdiff]
          simp only [sdiff_self, empty_prod, union_empty]
        · rw [prod_subset_prod_iff]
          exact Or.inl ⟨subset_rfl, subset_univ t⟩

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

Goal state before:
pp: α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × ℝ)
inst✝ : IsFiniteKernel κ
⊢ κ.fst ⊗ₖ κ.condKernelReal = κ

Tactic:
condKernelReal,

Goal state after:
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × ℝ)
inst✝ : IsFiniteKernel κ
⊢ κ.fst ⊗ₖ IsCondKernelCDF.toKernel κ.condKernelCDF ⋯ = κ
Module: Mathlib.Probability.Kernel.Disintegration.Unique

Goal state before:
pp: α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
ρ : Measure (α × Ω)
inst✝¹ : IsFiniteMeasure ρ
κ : Kernel α Ω
inst✝ : IsSFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
s : Set Ω
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
x✝ : ρ.fst t < ∞
⊢ ∫⁻ (x : α) in t, (κ x) s ∂ρ.fst = (ρ.fst ⊗ₘ κ) (t ×ˢ s)

Tactic:
exact (Measure.compProd_apply_prod ht hs).symm

Goal state after: