awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
X Y : Ω → E
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
h : X ⟂ᵢ[P] Y - X
this : IsProbabilityMeasure P
L : StrongDual ℝ E
h₁ :
  cexp ((↑(∫ (x : Ω), ((⇑L : (a : E) → ℝ) ∘ Y) x ∂P) : ℂ) * I - (↑Var[(⇑L : (a : E) → ℝ) ∘ Y; P] : ℂ) / 2) =
    cexp
      ((↑(∫ (a : Ω), HAdd.hAdd (α := ℝ) (((⇑L : (a : E) → ℝ) ∘ X) a) (((⇑L : (a : E) → ℝ) ∘ (Y - X)) a) ∂P) : ℂ) * I -
        (↑Var[HAdd.hAdd (α := Ω → ℝ) ((⇑L : (a : E) → ℝ) ∘ X) ((⇑L : (a : E) → ℝ) ∘ (Y - X)); P] : ℂ) / 2)
h₂ : MemLp (ε := ℝ) ((⇑L : (a : E) → ℝ) ∘ X) 2 P
⊢ charFunDual (mE := inst_2) (Measure.map X P) L * charFunDual (mE := inst_2) (Measure.map (Y - X) P) L =
    charFunDual (mE := inst_2) (Measure.map X P) L *
      cexp
        ((↑(∫ (x : Ω), ((⇑L : (a : E) → ℝ) ∘ (Y - X)) x ∂P) : ℂ) * I - (↑Var[(⇑L : (a : E) → ℝ) ∘ (Y - X); P] : ℂ) / 2)
have h₃ : MemLp (ε := ℝ) ((⇑L : (a : E) → ℝ) ∘ (Y - X)) 2 P
Tactic: rw [← Pi.mul_apply, ← h.charFunDual_map_add_eq_mul, add_sub_cancel, hX.charFunDual_map_eq,
    ← exp_add, sub_add_sub_comm, ← add_mul, ← ofReal_add, ← integral_add, ← add_div, ← ofReal_add,
    ← IndepFun.variance_add, hY.charFunDual_map_eq]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
X Y : Ω → E
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
h : X ⟂ᵢ[P] Y - X
this : IsProbabilityMeasure P
L : StrongDual ℝ E
h₁ :
  cexp ((↑(∫ (x : Ω), ((⇑L : (a : E) → ℝ) ∘ Y) x ∂P) : ℂ) * I - (↑Var[(⇑L : (a : E) → ℝ) ∘ Y; P] : ℂ) / 2) =
    cexp
      ((↑(∫ (a : Ω), HAdd.hAdd (α := ℝ) (((⇑L : (a : E) → ℝ) ∘ X) a) (((⇑L : (a : E) → ℝ) ∘ (Y - X)) a) ∂P) : ℂ) * I -
        (↑Var[HAdd.hAdd (α := Ω → ℝ) ((⇑L : (a : E) → ℝ) ∘ X) ((⇑L : (a : E) → ℝ) ∘ (Y - X)); P] : ℂ) / 2)
h₂ : MemLp (ε := ℝ) ((⇑L : (a : E) → ℝ) ∘ X) 2 P
h₃ : MemLp (ε := ℝ) ((⇑L : (a : E) → ℝ) ∘ (Y - X)) 2 P
⊢ charFunDual (mE := inst_2) (Measure.map X P) L * charFunDual (mE := inst_2) (Measure.map (Y - X) P) L =
    charFunDual (mE := inst_2) (Measure.map X P) L *
      cexp
        ((↑(∫ (x : Ω), ((⇑L : (a : E) → ℝ) ∘ (Y - X)) x ∂P) : ℂ) * I - (↑Var[(⇑L : (a : E) → ℝ) ∘ (Y - X); P] : ℂ) / 2)
have h₄ : ((⇑L : (a : E) → ℝ) ∘ X) ⟂ᵢ[P] (⇑L : (a : E) → ℝ) ∘ (Y - X)
Tactic: rw [← Pi.mul_apply, ← h.charFunDual_map_add_eq_mul, add_sub_cancel, hX.charFunDual_map_eq,
    ← exp_add, sub_add_sub_comm, ← add_mul, ← ofReal_add, ← integral_add, ← add_div, ← ofReal_add,
    ← IndepFun.variance_add, hY.charFunDual_map_eq]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
X Y : Ω → E
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
h : X ⟂ᵢ[P] Y - X
this : IsProbabilityMeasure P
L : StrongDual ℝ E
h₁ :
  cexp ((↑(∫ (x : Ω), ((⇑L : (a : E) → ℝ) ∘ Y) x ∂P) : ℂ) * I - (↑Var[(⇑L : (a : E) → ℝ) ∘ Y; P] : ℂ) / 2) =
    cexp
      ((↑(∫ (a : Ω), HAdd.hAdd (α := ℝ) (((⇑L : (a : E) → ℝ) ∘ X) a) (((⇑L : (a : E) → ℝ) ∘ (Y - X)) a) ∂P) : ℂ) * I -
        (↑Var[HAdd.hAdd (α := Ω → ℝ) ((⇑L : (a : E) → ℝ) ∘ X) ((⇑L : (a : E) → ℝ) ∘ (Y - X)); P] : ℂ) / 2)
h₂ : MemLp (ε := ℝ) ((⇑L : (a : E) → ℝ) ∘ X) 2 P
h₃ : MemLp (ε := ℝ) ((⇑L : (a : E) → ℝ) ∘ (Y - X)) 2 P
h₄ : ((⇑L : (a : E) → ℝ) ∘ X) ⟂ᵢ[P] (⇑L : (a : E) → ℝ) ∘ (Y - X)
⊢ charFunDual (mE := inst_2) (Measure.map X P) L * charFunDual (mE := inst_2) (Measure.map (Y - X) P) L =
    charFunDual (mE := inst_2) (Measure.map X P) L *
      cexp
        ((↑(∫ (x : Ω), ((⇑L : (a : E) → ℝ) ∘ (Y - X)) x ∂P) : ℂ) * I - (↑Var[(⇑L : (a : E) → ℝ) ∘ (Y - X); P] : ℂ) / 2)
have h₅ : Integrable (ε := ℝ) ((⇑L : (a : E) → ℝ) ∘ X) P
Tactic: rw [← Pi.mul_apply, ← h.charFunDual_map_add_eq_mul, add_sub_cancel, hX.charFunDual_map_eq,
    ← exp_add, sub_add_sub_comm, ← add_mul, ← ofReal_add, ← integral_add, ← add_div, ← ofReal_add,
    ← IndepFun.variance_add, hY.charFunDual_map_eq]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
X Y : Ω → E
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
h : X ⟂ᵢ[P] Y - X
this : IsProbabilityMeasure P
L : StrongDual ℝ E
h₁ :
  cexp ((↑(∫ (x : Ω), ((⇑L : (a : E) → ℝ) ∘ Y) x ∂P) : ℂ) * I - (↑Var[(⇑L : (a : E) → ℝ) ∘ Y; P] : ℂ) / 2) =
    cexp
      ((↑(∫ (a : Ω), HAdd.hAdd (α := ℝ) (((⇑L : (a : E) → ℝ) ∘ X) a) (((⇑L : (a : E) → ℝ) ∘ (Y - X)) a) ∂P) : ℂ) * I -
        (↑Var[HAdd.hAdd (α := Ω → ℝ) ((⇑L : (a : E) → ℝ) ∘ X) ((⇑L : (a : E) → ℝ) ∘ (Y - X)); P] : ℂ) / 2)
h₂ : MemLp (ε := ℝ) ((⇑L : (a : E) → ℝ) ∘ X) 2 P
h₃ : MemLp (ε := ℝ) ((⇑L : (a : E) → ℝ) ∘ (Y - X)) 2 P
h₄ : ((⇑L : (a : E) → ℝ) ∘ X) ⟂ᵢ[P] (⇑L : (a : E) → ℝ) ∘ (Y - X)
h₅ : Integrable (ε := ℝ) ((⇑L : (a : E) → ℝ) ∘ X) P
⊢ charFunDual (mE := inst_2) (Measure.map X P) L * charFunDual (mE := inst_2) (Measure.map (Y - X) P) L =
    charFunDual (mE := inst_2) (Measure.map X P) L *
      cexp
        ((↑(∫ (x : Ω), ((⇑L : (a : E) → ℝ) ∘ (Y - X)) x ∂P) : ℂ) * I - (↑Var[(⇑L : (a : E) → ℝ) ∘ (Y - X); P] : ℂ) / 2)
have h₆ : Integrable (ε := ℝ) ((⇑L : (a : E) → ℝ) ∘ (Y - X)) P
Tactic: rw [← Pi.mul_apply, ← h.charFunDual_map_add_eq_mul, add_sub_cancel, hX.charFunDual_map_eq,
    ← exp_add, sub_add_sub_comm, ← add_mul, ← ofReal_add, ← integral_add, ← add_div, ← ofReal_add,
    ← IndepFun.variance_add, hY.charFunDual_map_eq]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
X Y : Ω → E
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
h : X ⟂ᵢ[P] Y - X
this : IsProbabilityMeasure P
L : StrongDual ℝ E
h₁ :
  cexp ((↑(∫ (x : Ω), ((⇑L : (a : E) → ℝ) ∘ Y) x ∂P) : ℂ) * I - (↑Var[(⇑L : (a : E) → ℝ) ∘ Y; P] : ℂ) / 2) =
    cexp
      ((↑(∫ (a : Ω), HAdd.hAdd (α := ℝ) (((⇑L : (a : E) → ℝ) ∘ X) a) (((⇑L : (a : E) → ℝ) ∘ (Y - X)) a) ∂P) : ℂ) * I -
        (↑Var[HAdd.hAdd (α := Ω → ℝ) ((⇑L : (a : E) → ℝ) ∘ X) ((⇑L : (a : E) → ℝ) ∘ (Y - X)); P] : ℂ) / 2)
h₂ : MemLp (ε := ℝ) ((⇑L : (a : E) → ℝ) ∘ X) 2 P
h₃ : MemLp (ε := ℝ) ((⇑L : (a : E) → ℝ) ∘ (Y - X)) 2 P
h₄ : ((⇑L : (a : E) → ℝ) ∘ X) ⟂ᵢ[P] (⇑L : (a : E) → ℝ) ∘ (Y - X)
h₅ : Integrable (ε := ℝ) ((⇑L : (a : E) → ℝ) ∘ X) P
h₆ : Integrable (ε := ℝ) ((⇑L : (a : E) → ℝ) ∘ (Y - X)) P
⊢ charFunDual (mE := inst_2) (Measure.map X P) L * charFunDual (mE := inst_2) (Measure.map (Y - X) P) L =
    charFunDual (mE := inst_2) (Measure.map X P) L *
      cexp
        ((↑(∫ (x : Ω), ((⇑L : (a : E) → ℝ) ∘ (Y - X)) x ∂P) : ℂ) * I - (↑Var[(⇑L : (a : E) → ℝ) ∘ (Y - X); P] : ℂ) / 2)
have h₇ : AEMeasurable X P
Tactic: rw [← Pi.mul_apply, ← h.charFunDual_map_add_eq_mul, add_sub_cancel, hX.charFunDual_map_eq,
    ← exp_add, sub_add_sub_comm, ← add_mul, ← ofReal_add, ← integral_add, ← add_div, ← ofReal_add,
    ← IndepFun.variance_add, hY.charFunDual_map_eq]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
X Y : Ω → E
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
h : X ⟂ᵢ[P] Y - X
this : IsProbabilityMeasure P
L : StrongDual ℝ E
h₁ :
  cexp ((↑(∫ (x : Ω), ((⇑L : (a : E) → ℝ) ∘ Y) x ∂P) : ℂ) * I - (↑Var[(⇑L : (a : E) → ℝ) ∘ Y; P] : ℂ) / 2) =
    cexp
      ((↑(∫ (a : Ω), HAdd.hAdd (α := ℝ) (((⇑L : (a : E) → ℝ) ∘ X) a) (((⇑L : (a : E) → ℝ) ∘ (Y - X)) a) ∂P) : ℂ) * I -
        (↑Var[HAdd.hAdd (α := Ω → ℝ) ((⇑L : (a : E) → ℝ) ∘ X) ((⇑L : (a : E) → ℝ) ∘ (Y - X)); P] : ℂ) / 2)
h₂ : MemLp (ε := ℝ) ((⇑L : (a : E) → ℝ) ∘ X) 2 P
h₃ : MemLp (ε := ℝ) ((⇑L : (a : E) → ℝ) ∘ (Y - X)) 2 P
h₄ : ((⇑L : (a : E) → ℝ) ∘ X) ⟂ᵢ[P] (⇑L : (a : E) → ℝ) ∘ (Y - X)
h₅ : Integrable (ε := ℝ) ((⇑L : (a : E) → ℝ) ∘ X) P
h₆ : Integrable (ε := ℝ) ((⇑L : (a : E) → ℝ) ∘ (Y - X)) P
h₇ : AEMeasurable X P
⊢ charFunDual (mE := inst_2) (Measure.map X P) L * charFunDual (mE := inst_2) (Measure.map (Y - X) P) L =
    charFunDual (mE := inst_2) (Measure.map X P) L *
      cexp
        ((↑(∫ (x : Ω), ((⇑L : (a : E) → ℝ) ∘ (Y - X)) x ∂P) : ℂ) * I - (↑Var[(⇑L : (a : E) → ℝ) ∘ (Y - X); P] : ℂ) / 2)
have h₈ : AEMeasurable (Y - X) P
Tactic: rw [← Pi.mul_apply, ← h.charFunDual_map_add_eq_mul, add_sub_cancel, hX.charFunDual_map_eq,
    ← exp_add, sub_add_sub_comm, ← add_mul, ← ofReal_add, ← integral_add, ← add_div, ← ofReal_add,
    ← IndepFun.variance_add, hY.charFunDual_map_eq]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
X Y : Ω → E
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
h : X ⟂ᵢ[P] Y - X
this : IsProbabilityMeasure P
L : StrongDual ℝ E
⊢ cexp ((↑(∫ (x : Ω), ((⇑L : (a : E) → ℝ) ∘ Y) x ∂P) : ℂ) * I - (↑Var[(⇑L : (a : E) → ℝ) ∘ Y; P] : ℂ) / 2) =
    cexp
      ((↑(∫ (a : Ω), HAdd.hAdd (α := ℝ) (((⇑L : (a : E) → ℝ) ∘ X) a) (((⇑L : (a : E) → ℝ) ∘ (Y - X)) a) ∂P) : ℂ) * I -
        (↑Var[HAdd.hAdd (α := Ω → ℝ) ((⇑L : (a : E) → ℝ) ∘ X) ((⇑L : (a : E) → ℝ) ∘ (Y - X)); P] : ℂ) / 2)
have h₁ : ∀ (ω : Ω),
  ((⇑L : (a : E) → ℝ) ∘ Y) ω = HAdd.hAdd (α := ℝ) (((⇑L : (a : E) → ℝ) ∘ X) ω) (((⇑L : (a : E) → ℝ) ∘ (Y - X)) ω)
Tactic: congr with ω
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
X Y : Ω → E
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
h : X ⟂ᵢ[P] Y - X
this : IsProbabilityMeasure P
L : StrongDual ℝ E
h₁ :
  ∀ (ω : Ω),
    ((⇑L : (a : E) → ℝ) ∘ Y) ω = HAdd.hAdd (α := ℝ) (((⇑L : (a : E) → ℝ) ∘ X) ω) (((⇑L : (a : E) → ℝ) ∘ (Y - X)) ω)
⊢ cexp ((↑(∫ (x : Ω), ((⇑L : (a : E) → ℝ) ∘ Y) x ∂P) : ℂ) * I - (↑Var[(⇑L : (a : E) → ℝ) ∘ Y; P] : ℂ) / 2) =
    cexp
      ((↑(∫ (a : Ω), HAdd.hAdd (α := ℝ) (((⇑L : (a : E) → ℝ) ∘ X) a) (((⇑L : (a : E) → ℝ) ∘ (Y - X)) a) ∂P) : ℂ) * I -
        (↑Var[HAdd.hAdd (α := Ω → ℝ) ((⇑L : (a : E) → ℝ) ∘ X) ((⇑L : (a : E) → ℝ) ∘ (Y - X)); P] : ℂ) / 2)
have h₂ : ∀ (ω : Ω),
  ((⇑L : (a : E) → ℝ) ∘ Y) ω =
    HAdd.hAdd (α := Ω → ℝ) (β := Ω → ℝ) ((⇑L : (a : E) → ℝ) ∘ X) ((⇑L : (a : E) → ℝ) ∘ (Y - X)) ω
Tactic: congr with ω
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
X Y : Ω → E
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
h : X ⟂ᵢ[P] Y - X
this : IsProbabilityMeasure P
L : StrongDual ℝ E
⊢ AEMeasurable X P
have funProp : AEFinStronglyMeasurable.{u_1, u_2} (β := E) (fun (a : Ω) ↦ X a) P
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
X Y : Ω → E
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
h : X ⟂ᵢ[P] Y - X
this : IsProbabilityMeasure P
L : StrongDual ℝ E
⊢ AEMeasurable (Y - X) P
have funProp : AEFinStronglyMeasurable.{u_1, u_2} (β := E) (fun (a : Ω) ↦ Y a) P
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
X Y : Ω → E
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
h : X ⟂ᵢ[P] Y - X
this : IsProbabilityMeasure P
L : StrongDual ℝ E
funProp : AEFinStronglyMeasurable.{u_1, u_2} (β := E) (fun (a : Ω) ↦ Y a) P
⊢ AEMeasurable (Y - X) P
have funProp₁ : AEFinStronglyMeasurable.{u_1, u_2} (β := E) (fun (a : Ω) ↦ X a) P
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
X Y : Ω → E
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
h : X ⟂ᵢ[P] Y - X
this : IsProbabilityMeasure P
L : StrongDual ℝ E
⊢ MemLp (ε := ℝ) ((⇑L : (a : E) → ℝ) ∘ (Y - X)) 2 P
have h₁ : MemLp (HSub.hSub (α := Ω → ℝ) ((⇑L : (a : E) → ℝ) ∘ Y) ((⇑L : (a : E) → ℝ) ∘ X)) 2 P
Tactic: rw [map_comp_sub]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : 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 : (a : E) → ℝ) ∘ (Y - X)) P
have h₁ : Integrable (HSub.hSub (α := Ω → ℝ) ((⇑L : (a : E) → ℝ) ∘ Y) ((⇑L : (a : E) → ℝ) ∘ X)) P
Tactic: rw [map_comp_sub]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic (goal)
Goal:
T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : T → Ω → E
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : AddCommMonoid E
inst_3 : Module ℝ E
hX : IsGaussianProcess X P
hXY : ∀ (t : T), X t =ᶠ[ae P] Y t
I : Finset T
⊢ HasGaussianLaw (E := (i : ↥I) → E) (fun (ω : Ω) ↦ I.restrict (π := fun (x : T) ↦ E) fun (x : T) ↦ Y x ω) P
have isGaussian_map : IsGaussian (E := (i : ↥I) → E) (mE := MeasurableSpace.pi (X := fun (i : ↥I) ↦ E))
  (Measure.map (fun (ω : Ω) ↦ I.restrict (π := fun (x : T) ↦ E) fun (x : T) ↦ Y x ω) P)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic (goal)
Goal:
T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : T → Ω → E
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : AddCommMonoid E
inst_3 : Module ℝ E
hX : IsGaussianProcess X P
hXY : ∀ (t : T), X t =ᶠ[ae P] Y t
I : Finset T
⊢ IsGaussian (E := (i : ↥I) → E) (mE := MeasurableSpace.pi (X := fun (i : ↥I) ↦ E))
    (Measure.map (fun (ω : Ω) ↦ I.restrict (π := fun (x : T) ↦ E) fun (x : T) ↦ Y x ω) P)
have isGaussian_map : IsGaussian (E := (i : ↥I) → E) (mE := MeasurableSpace.pi (X := fun (i : ↥I) ↦ E))
  (Measure.map (fun (ω : Ω) ↦ I.restrict (π := fun (t : T) ↦ E) fun (x : T) ↦ X x ω) P)
Tactic: rw [map_restrict_eq_of_forall_ae_eq fun t ↦ (hXY t).symm]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic (goal)
Goal:
T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : NormedSpace ℝ E
inst_4 : SecondCountableTopology E
hX : IsGaussianProcess X P
I : Finset T
⊢ HasGaussianLaw.{u_3, u_4} (E := E) (∑ i ∈ I, X i) P
have h : Eq (α := Ω → E) (∑ i ∈ I, X i) (∑ i : ↥I, fun (ω : Ω) ↦ I.restrict (π := fun (x : T) ↦ E) (fun (x : T) ↦ X x ω) i)
Tactic: convert! (hX.hasGaussianLaw I).sum
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic (goal)
Goal:
T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : NormedSpace ℝ E
inst_4 : SecondCountableTopology E
hX : IsGaussianProcess X P
I : Finset T
⊢ HasGaussianLaw.{u_3, u_4} (E := E) (fun (ω : Ω) ↦ ∑ i ∈ I, X i ω) P
have h : ∀ (x : Ω), Eq.{u_4 + 1} (α := E) (∑ i ∈ I, X i x) ((∑ i ∈ I, X i) x)
Tactic: convert! hX.hasGaussianLaw_sum (I := I)
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic (goal)
Goal:
T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : NormedSpace ℝ E
inst_4 : SecondCountableTopology E
hX : IsGaussianProcess X P
n : ℕ
t : Fin (n + 1) → T
x y : ↥(image t univ) → E
⊢ (fun (i : Fin n) ↦
      (x + y) (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t i.succ) ⋯) -
        (x + y) (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t i.castSucc) ⋯)) =
    HAdd.hAdd (α := Fin n → E)
      (fun (i : Fin n) ↦
        x (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t i.succ) ⋯) -
          x (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t i.castSucc) ⋯))
      fun (i : Fin n) ↦
      y (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t i.succ) ⋯) -
        y (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t i.castSucc) ⋯)
have h : ∀ (x_1 : Fin n),
  (x + y) (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t x_1.succ) sorry) -
      (x + y) (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t x_1.castSucc) sorry) =
    HAdd.hAdd (α := Fin n → E) (β := Fin n → E)
      (fun (i : Fin n) ↦
        x (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t i.succ) sorry) -
          x (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t i.castSucc) sorry))
      (fun (i : Fin n) ↦
        y (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t i.succ) sorry) -
          y (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t i.castSucc) sorry))
      x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic (goal)
Goal:
T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : NormedSpace ℝ E
inst_4 : SecondCountableTopology E
hX : IsGaussianProcess X P
n : ℕ
t : Fin (n + 1) → T
x y : ↥(image t univ) → E
x_1 : Fin n
⊢ (x + y) (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t x_1.succ) ⋯) -
      (x + y) (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t x_1.castSucc) ⋯) =
    HAdd.hAdd (α := Fin n → E) (β := Fin n → E)
      (fun (i : Fin n) ↦
        x (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t i.succ) ⋯) -
          x (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t i.castSucc) ⋯))
      (fun (i : Fin n) ↦
        y (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t i.succ) ⋯) -
          y (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t i.castSucc) ⋯))
      x_1
have h : x (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t x_1.succ) sorry) +
      y (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t x_1.succ) sorry) -
    (x (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t x_1.castSucc) sorry) +
      y (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t x_1.castSucc) sorry)) =
  x (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t x_1.succ) sorry) -
      x (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t x_1.castSucc) sorry) +
    (y (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t x_1.succ) sorry) -
      y (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t x_1.castSucc) sorry))
Tactic: simp
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic (goal)
Goal:
T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : NormedSpace ℝ E
inst_4 : SecondCountableTopology E
hX : IsGaussianProcess X P
n : ℕ
t : Fin (n + 1) → T
m : ℝ
x : ↥(image t univ) → E
⊢ (fun (i : Fin n) ↦
      (m • x) (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t i.succ) ⋯) -
        (m • x) (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t i.castSucc) ⋯)) =
    HSMul.hSMul (α := ℝ) (β := Fin n → E) ((RingHom.id ℝ : (a : ℝ) → ℝ) m : ℝ) fun (i : Fin n) ↦
      x (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t i.succ) ⋯) -
        x (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t i.castSucc) ⋯)
have h : ∀ (x_1 : Fin n),
  (m • x) (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t x_1.succ) sorry) -
      (m • x) (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t x_1.castSucc) sorry) =
    HSMul.hSMul (α := ℝ) (β := Fin n → E) ((RingHom.id ℝ : (a : ℝ) → ℝ) m : ℝ)
      (fun (i : Fin n) ↦
        x (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t i.succ) sorry) -
          x (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t i.castSucc) sorry))
      x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic (goal)
Goal:
T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : NormedSpace ℝ E
inst_4 : SecondCountableTopology E
hX : IsGaussianProcess X P
n : ℕ
t : Fin (n + 1) → T
m : ℝ
x : ↥(image t univ) → E
x_1 : Fin n
⊢ (m • x) (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t x_1.succ) ⋯) -
      (m • x) (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t x_1.castSucc) ⋯) =
    HSMul.hSMul (α := ℝ) (β := Fin n → E) ((RingHom.id ℝ : (a : ℝ) → ℝ) m : ℝ)
      (fun (i : Fin n) ↦
        x (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t i.succ) ⋯) -
          x (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t i.castSucc) ⋯))
      x_1
have h : m • x (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t x_1.succ) sorry) -
    m • x (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t x_1.castSucc) sorry) =
  m •
    (x (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t x_1.succ) sorry) -
      x (Subtype.mk (p := fun (x : T) ↦ x ∈ image t univ) (t x_1.castSucc) sorry))
Tactic: simp
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic (goal)
Goal:
S : Type u_1
T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : NormedSpace ℝ E
inst_4 : SecondCountableTopology E
F : Type u_6
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace ℝ F
inst_7 : MeasurableSpace F
inst_8 : BorelSpace F
inst_9 : SecondCountableTopology F
Y : S → Ω → F
hX : IsGaussianProcess X P
h :
  ∀ (s : S),
    ∃ (I : Finset T) (L : (↥I → E) →L[ℝ] F),
      ∀ (ω : Ω), Y s ω = (L : (a : ↥I → E) → F) (I.restrict (π := fun (x : T) ↦ E) fun (x : T) ↦ X x ω : (i : ↥I) → E)
I : Finset S
⊢ HasGaussianLaw (E := (i : ↥I) → F) (fun (ω : Ω) ↦ I.restrict (π := fun (x : S) ↦ F) fun (x : S) ↦ Y x ω) P
have choose : ∀ (J : (s : S) → Finset T) (L : (s : S) → (↥(J s) → E) →L[ℝ] F)
  (hL :
    ∀ (s : S) (ω : Ω),
      Y s ω =
        (L s : (a : ↥(J s) → E) → F) ((J s).restrict (π := fun (x : T) ↦ E) fun (x : T) ↦ X x ω : (i : ↥(J s)) → E)),
  HasGaussianLaw (E := (i : ↥I) → F) (fun (ω : Ω) ↦ I.restrict (π := fun (x : S) ↦ F) fun (x : S) ↦ Y x ω) P
Tactic: choose J L hL using h
Cleared hypotheses: h