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

Goal state before:
pp: case pos
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁷ : Nonempty ι
τ : Ω → WithTop ι
inst✝⁶ : LinearOrder ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
inst✝² : SecondCountableTopology ι
inst✝¹ : BorelSpace ι
f : Filtration ι m
inst✝ : PseudoMetrizableSpace ι
hτ : IsStoppingTime f τ
i : ι
m_prod : MeasurableSpace (↑(Set.Iic i) × Ω) := Subtype.instMeasurableSpace.prod (↑f i)
m_set : (t : Set (↑(Set.Iic i) × Ω)) → MeasurableSpace ↑t := fun x ↦ Subtype.instMeasurableSpace
s : Set (↑(Set.Iic i) × Ω) := {p | τ p.2 ≤ ↑i}
hs : MeasurableSet s
h_meas_fst : ∀ (t : Set (↑(Set.Iic i) × Ω)), Measurable fun x ↦ ↑(↑x).1
sc : Set (↑(Set.Iic i) × Ω) := sᶜ
ω : ↑sc
hx_fst_le : ↑(↑ω).1 ≤ i
h : τ (↑ω).2 = ⊤
⊢ ↑↑(↑ω).1 ≤ τ (↑ω).2

pp: case neg
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁷ : Nonempty ι
τ : Ω → WithTop ι
inst✝⁶ : LinearOrder ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
inst✝² : SecondCountableTopology ι
inst✝¹ : BorelSpace ι
f : Filtration ι m
inst✝ : PseudoMetrizableSpace ι
hτ : IsStoppingTime f τ
i : ι
m_prod : MeasurableSpace (↑(Set.Iic i) × Ω) := Subtype.instMeasurableSpace.prod (↑f i)
m_set : (t : Set (↑(Set.Iic i) × Ω)) → MeasurableSpace ↑t := fun x ↦ Subtype.instMeasurableSpace
s : Set (↑(Set.Iic i) × Ω) := {p | τ p.2 ≤ ↑i}
hs : MeasurableSet s
h_meas_fst : ∀ (t : Set (↑(Set.Iic i) × Ω)), Measurable fun x ↦ ↑(↑x).1
sc : Set (↑(Set.Iic i) × Ω) := sᶜ
ω : ↑sc
hx_fst_le : ↑(↑ω).1 ≤ i
h : ¬τ (↑ω).2 = ⊤
⊢ ↑↑(↑ω).1 ≤ τ (↑ω).2

Tactic:
· simp [h]

Goal state after:
case neg
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁷ : Nonempty ι
τ : Ω → WithTop ι
inst✝⁶ : LinearOrder ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
inst✝² : SecondCountableTopology ι
inst✝¹ : BorelSpace ι
f : Filtration ι m
inst✝ : PseudoMetrizableSpace ι
hτ : IsStoppingTime f τ
i : ι
m_prod : MeasurableSpace (↑(Set.Iic i) × Ω) := Subtype.instMeasurableSpace.prod (↑f i)
m_set : (t : Set (↑(Set.Iic i) × Ω)) → MeasurableSpace ↑t := fun x ↦ Subtype.instMeasurableSpace
s : Set (↑(Set.Iic i) × Ω) := {p | τ p.2 ≤ ↑i}
hs : MeasurableSet s
h_meas_fst : ∀ (t : Set (↑(Set.Iic i) × Ω)), Measurable fun x ↦ ↑(↑x).1
sc : Set (↑(Set.Iic i) × Ω) := sᶜ
ω : ↑sc
hx_fst_le : ↑(↑ω).1 ≤ i
h : ¬τ (↑ω).2 = ⊤
⊢ ↑↑(↑ω).1 ≤ τ (↑ω).2
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
hX : ¬Integrable (fun ω ↦ rexp (t * X ω)) μ
⊢ mgf X μ t = 0

Tactic:
simp only [mgf, integral_undef hX]

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 τ
t : Set β
ht : MeasurableSet t
i : ι
⊢ MeasurableSet (stoppedValue u τ ⁻¹' t ∩ {ω | τ ω ≤ ↑i})

Tactic:
have h_str_meas : ∀ i, StronglyMeasurable[f i] (stoppedValue u fun ω => min (τ ω) i) := fun i =>
    stronglyMeasurable_stoppedValue_of_le hf_prog (hτ.min_const i) fun _ => min_le_right _ _
  suffices stoppedValue u τ ⁻¹' t ∩ {ω : Ω | τ ω ≤ i} =
      (stoppedValue u fun ω => min (τ ω) i) ⁻¹' t ∩ {ω : Ω | τ ω ≤ i} by
    rw [this]; exact ((h_str_meas i).measurable ht).inter (hτ.measurableSet_le i)
  ext1 ω
  simp only [stoppedValue, Set.mem_inter_iff, Set.mem_preimage, Set.mem_ofPred_eq,
    and_congr_left_iff]
  intro h
  rw [min_eq_left h]

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

Goal state before:
pp: case e_f
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t α : ℝ
x : Ω
⊢ rexp (t * (α + X x)) = rexp (t * α) * rexp (t * X x)

Tactic:
rw [mul_add, exp_add]

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

Goal state before:
pp: case pos
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X Y : Ω → ℝ
h_indep : X ⟂ᵢ[μ] Y
h_int_X : Integrable (fun ω ↦ rexp (t * X ω)) μ
h_int_Y : Integrable (fun ω ↦ rexp (t * Y ω)) μ
hμ : μ = 0
⊢ cgf (X + Y) μ t = cgf X μ t + cgf Y μ t

pp: case neg
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X Y : Ω → ℝ
h_indep : X ⟂ᵢ[μ] Y
h_int_X : Integrable (fun ω ↦ rexp (t * X ω)) μ
h_int_Y : Integrable (fun ω ↦ rexp (t * Y ω)) μ
hμ : ¬μ = 0
⊢ cgf (X + Y) μ t = cgf X μ t + cgf Y μ t

Tactic:
· simp [hμ]

Goal state after:
case neg
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X Y : Ω → ℝ
h_indep : X ⟂ᵢ[μ] Y
h_int_X : Integrable (fun ω ↦ rexp (t * X ω)) μ
h_int_Y : Integrable (fun ω ↦ rexp (t * Y ω)) μ
hμ : ¬μ = 0
⊢ cgf (X + Y) μ t = cgf X μ t + cgf Y μ t
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: case inl
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
ε : ℝ
ht : 0 ≤ t
h_int : Integrable (fun ω ↦ rexp (t * X ω)) μ
ht_zero_eq : 0 = t
⊢ μ.real {ω | ε ≤ X ω} ≤ rexp (-t * ε) * mgf X μ t

Tactic:
ht_zero_eq.symm

Goal state after:
case inl
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
ε : ℝ
ht : 0 ≤ t
h_int : Integrable (fun ω ↦ rexp (t * X ω)) μ
ht_zero_eq : 0 = t
⊢ μ.real {ω | ε ≤ X ω} ≤ rexp (-0 * ε) * mgf X μ 0
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht_int_pos : Integrable (fun ω ↦ rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (fun ω ↦ rexp ((v - t) * X ω)) μ
⊢ Integrable (fun ω ↦ rexp (|t| * |X ω| + v * X ω)) μ

Tactic:
rcases le_total 0 t with ht_nonneg | ht_nonpos
  · simp_rw [abs_of_nonneg ht_nonneg]
    exact integrable_exp_mul_abs_add ht_int_pos ht_int_neg
  · simp_rw [abs_of_nonpos ht_nonpos]
    exact integrable_exp_mul_abs_add ht_int_neg (by simpa using ht_int_pos)

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

Goal state before:
pp: case h
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ∞
inst✝ : AddCommMonoid β
n : ℕ
x : Ω
h₁ : τ x = ↑n
h₂ : ↑n + 1 ≤ τ x
⊢ False

Tactic:
h₁

Goal state after:
case h
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ∞
inst✝ : AddCommMonoid β
n : ℕ
x : Ω
h₁ : τ x = ↑n
h₂ : ↑n + 1 ≤ ↑n
⊢ False
Module: Mathlib.Probability.Moments.MGFAnalytic

Goal state before:
pp: case pos
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : μ = 0
⊢ deriv (deriv (cgf X μ)) v = (∫ (x : Ω), (fun ω ↦ X ω ^ 2 * rexp (v * X ω)) x ∂μ) / mgf X μ v - deriv (cgf X μ) v ^ 2

pp: case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
⊢ deriv (deriv (cgf X μ)) v = (∫ (x : Ω), (fun ω ↦ X ω ^ 2 * rexp (v * X ω)) x ∂μ) / mgf X μ v - deriv (cgf X μ) v ^ 2

Tactic:
· simp [hμ]

Goal state after:
case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
⊢ deriv (deriv (cgf X μ)) v = (∫ (x : Ω), (fun ω ↦ X ω ^ 2 * rexp (v * X ω)) x ∂μ) / mgf X μ v - deriv (cgf X μ) v ^ 2
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: case refine_2
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht : t ≠ 0
ht_int_pos : Integrable (fun ω ↦ rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (fun ω ↦ rexp ((v - t) * X ω)) μ
p : ℝ
hp : 0 ≤ p
hX : AEMeasurable X μ
⊢ Integrable (fun a ↦ |X a ^ p| * rexp (v * X a)) μ

Tactic:
have h := integrable_rpow_abs_mul_exp_of_integrable_exp_mul ht ht_int_pos ht_int_neg hp

Goal state after:
case refine_2
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht : t ≠ 0
ht_int_pos : Integrable (fun ω ↦ rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (fun ω ↦ rexp ((v - t) * X ω)) μ
p : ℝ
hp : 0 ≤ p
hX : AEMeasurable X μ
h : Integrable (fun ω ↦ |X ω| ^ p * rexp (v * X ω)) μ
⊢ Integrable (fun a ↦ |X a ^ p| * rexp (v * X a)) μ
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < min (v - l) (u - v)
⊢ v - (v - l) ≤ v - min (v - l) (u - v)

Tactic:
by gcongr; exact inf_le_left

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

Goal state before:
pp: case pos
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : μ = 0
⊢ iteratedDeriv 2 (cgf X μ) v = (∫ (x : Ω), (fun ω ↦ (X ω - deriv (cgf X μ) v) ^ 2 * rexp (v * X ω)) x ∂μ) / mgf X μ v

pp: case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
⊢ iteratedDeriv 2 (cgf X μ) v = (∫ (x : Ω), (fun ω ↦ (X ω - deriv (cgf X μ) v) ^ 2 * rexp (v * X ω)) x ∂μ) / mgf X μ v

Tactic:
· simp [hμ]

Goal state after:
case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
⊢ iteratedDeriv 2 (cgf X μ) v = (∫ (x : Ω), (fun ω ↦ (X ω - deriv (cgf X μ) v) ^ 2 * rexp (v * X ω)) x ∂μ) / mgf X μ v
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: case pos
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : 0 ∈ interior (integrableExpSet X μ)
p : ℝ≥0
hX : AEMeasurable X μ
hp_zero : p = 0
⊢ MemLp X (↑p) μ

Tactic:
simp only [hp_zero, ENNReal.coe_zero, memLp_zero_iff_aestronglyMeasurable]

Goal state after:
case pos
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : 0 ∈ interior (integrableExpSet X μ)
p : ℝ≥0
hX : AEMeasurable X μ
hp_zero : p = 0
⊢ AEStronglyMeasurable X μ
Module: Mathlib.Probability.Moments.CovarianceBilin

Goal state before:
pp: case neg
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : CompleteSpace E
hμ : ¬MemLp id 2 μ
⊢ (↑(covarianceOperator μ)).IsPositive

pp: case pos
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : CompleteSpace E
hμ : MemLp id 2 μ
⊢ (↑(covarianceOperator μ)).IsPositive

Tactic:
· simp [hμ]

Goal state after:
case pos
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : CompleteSpace E
hμ : MemLp id 2 μ
⊢ (↑(covarianceOperator μ)).IsPositive
Module: Mathlib.Probability.Moments.CovarianceBilinDual

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
mE : MeasurableSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : BorelSpace E
⊢ covarianceBilinDual 0 = 0

Tactic:
by
  rw [covarianceBilinDual, Measure.map_zero, uncenteredCovarianceBilinDual_zero]

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

Goal state before:
pp: case neg
E : Type u_1
inst✝² : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝¹ : NormedSpace ℝ E
inst✝ : BorelSpace E
L : StrongDual ℝ E
h : ¬MemLp id 2 μ
⊢ 0 ≤ ((covarianceBilinDual μ) L) L

Tactic:
· simp [h]

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

Goal state before:
pp: E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
t : E
⊢ ∏ x, cexp (-(↑⟪(stdOrthonormalBasis ℝ E) x, t⟫ ^ 2 / 2)) = cexp (-↑‖t‖ ^ 2 / 2)

Tactic:
simp_rw [← exp_sum, Finset.sum_neg_distrib, ← Finset.sum_div, ← ofReal_pow,
    ← ofReal_sum, (stdOrthonormalBasis ℝ E).sum_sq_inner_right, neg_div]

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

Goal state before:
pp: ι : Type u_1
inst✝⁵ : Fintype ι
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
⊢ IsGaussian (stdGaussian E)

Tactic:
refine isGaussian_iff_gaussian_charFun.2 ⟨0, innerSL ℝ,
    LinearMap.BilinForm.isPosSemidef_iff.2 isPosSemidef_inner, ?_⟩

Goal state after:
ι : Type u_1
inst✝⁵ : Fintype ι
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
⊢ ∀ (t : E), charFun (stdGaussian E) t = cexp (↑⟪t, 0⟫ * I - ↑(((innerSL ℝ) t) t) / 2)
Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic

Goal state before:
pp: Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
X : Ω → E
inst✝ : InnerProductSpace ℝ E
t : E
hX : HasGaussianLaw X P
⊢ charFun (Measure.map X P) t = cexp (↑(∫ (x : Ω), (fun ω ↦ ⟪t, X ω⟫) x ∂P) * I - ↑Var[fun ω ↦ ⟪t, X ω⟫; P] / 2)

Tactic:
rw [hX.isGaussian_map.charFun_eq, integral_map hX.aemeasurable (by fun_prop),
    variance_map (by fun_prop) hX.aemeasurable, integral_complex_ofReal, Function.comp_def]

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

Goal state before:
pp: Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
X : Ω → E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
hX : HasGaussianLaw X P
p : ℝ≥0∞
hp : p ≠ ∞
⊢ MemLp X p P

Tactic:
← Function.id_comp X,

Goal state after:
Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
X : Ω → E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
hX : HasGaussianLaw X P
p : ℝ≥0∞
hp : p ≠ ∞
⊢ MemLp (id ∘ X) p P
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✝ : InnerProductSpace ℝ E
mX : ∀ i ∈ s, AEMeasurable (X i) P
hX : iIndepFun (s.restrict X) P
x✝ : E
⊢ charFun (Measure.map (∑ i ∈ s, X i) P) x✝ = (∏ i ∈ s, charFun (Measure.map (X i) P)) x✝

Tactic:
simp [charFun_eq_charFunDual_toDualMap, hX.charFunDual_map_finsetSum_eq_prod mX]

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
E : ι → Type u_3
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace ℝ (E i)
L✝ L : (i : ι) → StrongDual ℝ (E i) →L[ℝ] StrongDual ℝ (E i) →L[ℝ] ℝ
x y z : StrongDual ℝ ((i : ι) → E i)
⊢ ∑ i, ((L i) ((x + y) ∘SL single ℝ E i)) (z ∘SL single ℝ E i) =
    ∑ i, ((L i) (x ∘SL single ℝ E i)) (z ∘SL single ℝ E i) + ∑ i, ((L i) (y ∘SL single ℝ E i)) (z ∘SL single ℝ E i)

Tactic:
by simp [sum_add_distrib]

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
E : ι → Type u_3
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace ℝ (E i)
L✝ L : (i : ι) → StrongDual ℝ (E i) →L[ℝ] StrongDual ℝ (E i) →L[ℝ] ℝ
x y z : StrongDual ℝ ((i : ι) → E i)
⊢ ∑ i, ((L i) (x ∘SL single ℝ E i)) ((y + z) ∘SL single ℝ E i) =
    ∑ i, ((L i) (x ∘SL single ℝ E i)) (y ∘SL single ℝ E i) + ∑ i, ((L i) (x ∘SL single ℝ E i)) (z ∘SL single ℝ E i)

Tactic:
by simp [sum_add_distrib]

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

Goal state before:
pp: ⊢ ∃ a, ∀ b ≤ a, 0 = defaultRatCDF b

Tactic:
refine ⟨-1, fun q hq => (if_pos (hq.trans_lt ?_)).symm⟩

Goal state after:
q : ℚ
hq : q ≤ -1
⊢ -1 < 0
Module: Mathlib.Probability.Kernel.Disintegration.CondCDF

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
s : Set α
hs : MeasurableSet s
⊢ Tendsto (fun r ↦ (ρ.IicSnd ↑r) s) atTop (𝓝 (ρ.fst s))

Tactic:
simp_rw [ρ.IicSnd_apply _ hs, fst_apply hs, ← prod_univ]

Goal state after:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
s : Set α
hs : MeasurableSet s
⊢ Tendsto (fun r ↦ ρ (s ×ˢ Iic ↑r)) atTop (𝓝 (ρ (s ×ˢ univ)))
Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst✝⁶ : Finite ι
E : ι → Type u_3
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → MeasurableSpace (E i)
inst✝³ : ∀ (i : ι), CompleteSpace (E i)
inst✝² : ∀ (i : ι), BorelSpace (E i)
inst✝¹ : ∀ (i : ι), SecondCountableTopology (E i)
inst✝ : (i : ι) → NormedSpace ℝ (E i)
X : (i : ι) → Ω → E i
hX : HasGaussianLaw (fun ω i ↦ X i ω) P
h :
  ∀ (i j : ι),
    i ≠ j → ∀ (L₁ : StrongDual ℝ (E i)) (L₂ : StrongDual ℝ (E j)), cov[fun x ↦ L₁ (X i x), fun x ↦ L₂ (X j x); P] = 0
this✝¹ : IsProbabilityMeasure P
this✝ : Fintype ι := Fintype.ofFinite ι
L : StrongDual ℝ ((x : ι) → E x)
this : ∀ (ω : Ω), (L fun x ↦ X x ω) = ∑ i, (L ∘SL single ℝ E i) (X i ω)
⊢ cexp (↑(∫ (ω : Ω), L fun i ↦ X i ω ∂P) * I - ↑Var[fun ω ↦ L fun i ↦ X i ω; P] / 2) =
    ∏ i, charFunDual (Measure.map (fun x ↦ X i x) P) (L ∘SL single ℝ E i)

Tactic:
fun i ↦ (hX.eval i).charFunDual_map_eq_fun,

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst✝⁶ : Finite ι
E : ι → Type u_3
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → MeasurableSpace (E i)
inst✝³ : ∀ (i : ι), CompleteSpace (E i)
inst✝² : ∀ (i : ι), BorelSpace (E i)
inst✝¹ : ∀ (i : ι), SecondCountableTopology (E i)
inst✝ : (i : ι) → NormedSpace ℝ (E i)
X : (i : ι) → Ω → E i
hX : HasGaussianLaw (fun ω i ↦ X i ω) P
h :
  ∀ (i j : ι),
    i ≠ j → ∀ (L₁ : StrongDual ℝ (E i)) (L₂ : StrongDual ℝ (E j)), cov[fun x ↦ L₁ (X i x), fun x ↦ L₂ (X j x); P] = 0
this✝¹ : IsProbabilityMeasure P
this✝ : Fintype ι := Fintype.ofFinite ι
L : StrongDual ℝ ((x : ι) → E x)
this : ∀ (ω : Ω), (L fun x ↦ X x ω) = ∑ i, (L ∘SL single ℝ E i) (X i ω)
⊢ cexp (↑(∫ (ω : Ω), L fun i ↦ X i ω ∂P) * I - ↑Var[fun ω ↦ L fun i ↦ X i ω; P] / 2) =
    ∏ x, cexp (↑(∫ (ω : Ω), (L ∘SL single ℝ E x) (X x ω) ∂P) * I - ↑Var[fun ω ↦ (L ∘SL single ℝ E x) (X x ω); P] / 2)
Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst✝⁶ : Finite ι
E : ι → Type u_3
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → MeasurableSpace (E i)
inst✝³ : ∀ (i : ι), CompleteSpace (E i)
inst✝² : ∀ (i : ι), BorelSpace (E i)
inst✝¹ : ∀ (i : ι), SecondCountableTopology (E i)
inst✝ : (i : ι) → NormedSpace ℝ (E i)
X : (i : ι) → Ω → E i
hX : HasGaussianLaw (fun ω i ↦ X i ω) P
h :
  ∀ (i j : ι),
    i ≠ j → ∀ (L₁ : StrongDual ℝ (E i)) (L₂ : StrongDual ℝ (E j)), cov[fun x ↦ L₁ (X i x), fun x ↦ L₂ (X j x); P] = 0
this✝¹ : IsProbabilityMeasure P
this✝ : Fintype ι := Fintype.ofFinite ι
L : StrongDual ℝ ((x : ι) → E x)
this : ∀ (ω : Ω), (L fun x ↦ X x ω) = ∑ i, (L ∘SL single ℝ E i) (X i ω)
⊢ charFunDual (Measure.map (fun ω x ↦ X x ω) P) L =
    ∏ i, charFunDual (Measure.map (fun x ↦ X i x) P) (L ∘SL single ℝ E i)

Tactic:
simp_rw [hX.charFunDual_map_eq_fun, fun i ↦ (hX.eval i).charFunDual_map_eq_fun, ← Complex.exp_sum,
    sum_sub_distrib, ← sum_mul, this]

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst✝⁶ : Finite ι
E : ι → Type u_3
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → MeasurableSpace (E i)
inst✝³ : ∀ (i : ι), CompleteSpace (E i)
inst✝² : ∀ (i : ι), BorelSpace (E i)
inst✝¹ : ∀ (i : ι), SecondCountableTopology (E i)
inst✝ : (i : ι) → NormedSpace ℝ (E i)
X : (i : ι) → Ω → E i
hX : HasGaussianLaw (fun ω i ↦ X i ω) P
h :
  ∀ (i j : ι),
    i ≠ j → ∀ (L₁ : StrongDual ℝ (E i)) (L₂ : StrongDual ℝ (E j)), cov[fun x ↦ L₁ (X i x), fun x ↦ L₂ (X j x); P] = 0
this✝¹ : IsProbabilityMeasure P
this✝ : Fintype ι := Fintype.ofFinite ι
L : StrongDual ℝ ((x : ι) → E x)
this : ∀ (ω : Ω), (L fun x ↦ X x ω) = ∑ i, (L ∘SL single ℝ E i) (X i ω)
⊢ cexp
      (↑(∫ (ω : Ω), ∑ i, (L ∘SL single ℝ E i) (X i ω) ∂P) * I -
        ↑Var[fun ω ↦ ∑ i, (L ∘SL single ℝ E i) (X i ω); P] / 2) =
    cexp
      ((∑ i, ↑(∫ (ω : Ω), (L ∘SL single ℝ E i) (X i ω) ∂P)) * I -
        ∑ x, ↑Var[fun ω ↦ (L ∘SL single ℝ E x) (X x ω); P] / 2)
Module: Mathlib.Probability.Kernel.Disintegration.CondCDF

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
a✝ : Unit
r r' : ℚ
hrr' : r ≤ r'
a : α
⊢ (Monotone fun r ↦ preCDF ρ r a) → (∀ (r : ℚ), preCDF ρ r a ≤ 1) → (preCDF ρ r a).toReal ≤ (preCDF ρ r' a).toReal

Tactic:
h₁

Goal state after:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
a✝ : Unit
r r' : ℚ
hrr' : r ≤ r'
a : α
h₁ : Monotone fun r ↦ preCDF ρ r a
⊢ (∀ (r : ℚ), preCDF ρ r a ≤ 1) → (preCDF ρ r a).toReal ≤ (preCDF ρ r' a).toReal
Module: Mathlib.Probability.CDF

Goal state before:
pp: μ : Measure ℝ
inst✝ : IsProbabilityMeasure μ
x : ℝ
⊢ ↑(cdf μ) x = μ.real (Iic x)

Tactic:
rw [measureReal_def, ← ofReal_cdf μ x, ENNReal.toReal_ofReal (cdf_nonneg μ x)]

Goal state after:
Module: Mathlib.Probability.Kernel.Composition.Lemmas

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst✝ : SFinite μ
hκ : IsSFiniteKernel κ
⊢ ⇑(Kernel.id ∥ₖ κ ∘ₖ Kernel.copy α) ∘ₘ μ = ⇑(Kernel.id ∥ₖ κ) ∘ₘ ⇑(Kernel.copy α) ∘ₘ μ

Tactic:
Measure.comp_assoc

Goal state after:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst✝ : SFinite μ
hκ : IsSFiniteKernel κ
⊢ ⇑(Kernel.id ∥ₖ κ ∘ₖ Kernel.copy α) ∘ₘ μ = ⇑(Kernel.id ∥ₖ κ ∘ₖ Kernel.copy α) ∘ₘ μ
Module: Mathlib.Probability.Kernel.Composition.Lemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
κ : Kernel β γ
inst✝ : IsSFiniteKernel κ
s : Set (α × γ)
hs : MeasurableSet s
⊢ ∫⁻ (x : α), (⇑κ ∘ₘ ν) (Prod.mk x ⁻¹' s) ∂μ = ∫⁻ (a : α × β), ((Kernel.id ∥ₖ κ) a) s ∂μ.prod ν

Tactic:
Measure.bind_apply (measurable_prodMk_left hs) (Kernel.aemeasurable _)

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
κ : Kernel β γ
inst✝ : IsSFiniteKernel κ
s : Set (α × γ)
hs : MeasurableSet s
⊢ ∫⁻ (x : α), ∫⁻ (a : β), (κ a) (Prod.mk x ⁻¹' s) ∂ν ∂μ = ∫⁻ (a : α × β), ((Kernel.id ∥ₖ κ) a) s ∂μ.prod ν
Module: Mathlib.Probability.Kernel.Composition.Lemmas

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel β γ
inst✝ : IsSFiniteKernel η
hμ : ¬SFinite μ
⊢ ⇑(Kernel.id ∥ₖ η) ∘ₘ μ ⊗ₘ κ = μ ⊗ₘ (η ∘ₖ κ)

pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel β γ
inst✝ : IsSFiniteKernel η
hμ : SFinite μ
⊢ ⇑(Kernel.id ∥ₖ η) ∘ₘ μ ⊗ₘ κ = μ ⊗ₘ (η ∘ₖ κ)

Tactic:
· simp [hμ]

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel β γ
inst✝ : IsSFiniteKernel η
hμ : SFinite μ
⊢ ⇑(Kernel.id ∥ₖ η) ∘ₘ μ ⊗ₘ κ = μ ⊗ₘ (η ∘ₖ κ)
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 α γ
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
⊢ Measurable fun x ↦ κ.densityProcess ν n a x s

Tactic:
refine @Measurable.ennreal_toReal _ (countableFiltration γ n) _ ?_
  -- The exact also works without the `( :)`, but is a bit slow.
  exact ((measurable_densityProcess_countableFiltration_aux κ ν n hs).comp measurable_prodMk_left :)

Goal state after: