awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
μ : Measure E
inst_4 : IsFiniteMeasure μ
h :
  ∀ (L : StrongDual ℝ E),
    charFunDual μ L = cexp ((∫ (x : E), (↑((L : (a : E) → ℝ) x) : ℂ) ∂μ) * I - (↑Var[(⇑L : (a : E) → ℝ); μ] : ℂ) / 2)
L : StrongDual ℝ E
u : ℝ
⊢ ∫ (x : E), (↑u : ℂ) * (↑((L : (a : E) → ℝ) x) : ℂ) ∂μ = (↑u : ℂ) * (↑(∫ (x : E), (L : (a : E) → ℝ) x ∂μ) : ℂ)
have h₁ : (↑u : ℂ) * ∫ (a : E), (↑((L : (a : E) → ℝ) a) : ℂ) ∂μ = (↑u : ℂ) * (↑(∫ (x : E), (L : (a : E) → ℝ) x ∂μ) : ℂ)
Tactic: rw [integral_const_mul, integral_complex_ofReal]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
μ : Measure E
inst_4 : IsFiniteMeasure μ
h :
  ∀ (L : StrongDual ℝ E),
    charFunDual μ L = cexp ((∫ (x : E), (↑((L : (a : E) → ℝ) x) : ℂ) ∂μ) * I - (↑Var[(⇑L : (a : E) → ℝ); μ] : ℂ) / 2)
L : StrongDual ℝ E
u : ℝ
h₁ : (↑u : ℂ) * ∫ (a : E), (↑((L : (a : E) → ℝ) a) : ℂ) ∂μ = (↑u : ℂ) * (↑(∫ (x : E), (L : (a : E) → ℝ) x ∂μ) : ℂ)
⊢ ∫ (x : E), (↑u : ℂ) * (↑((L : (a : E) → ℝ) x) : ℂ) ∂μ = (↑u : ℂ) * (↑(∫ (x : E), (L : (a : E) → ℝ) x ∂μ) : ℂ)
have h₂ : (↑u : ℂ) * (↑(∫ (x : E), (L : (a : E) → ℝ) x ∂μ) : ℂ) = (↑u : ℂ) * (↑(∫ (x : E), (L : (a : E) → ℝ) x ∂μ) : ℂ)
Tactic: rw [integral_const_mul, integral_complex_ofReal]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
μ : Measure E
inst_4 : IsFiniteMeasure μ
h :
  ∀ (L : StrongDual ℝ E),
    charFunDual μ L = cexp ((∫ (x : E), (↑((L : (a : E) → ℝ) x) : ℂ) ∂μ) * I - (↑Var[(⇑L : (a : E) → ℝ); μ] : ℂ) / 2)
L : StrongDual ℝ E
u : ℝ
⊢ (↑Var[HSMul.hSMul (β := (a : E) → ℝ) u (⇑L : (a : E) → ℝ); μ] : ℂ) =
    (↑(max Var[(⇑L : (a : E) → ℝ); μ] 0) : ℂ) * HPow.hPow (β := ℕ) (↑u : ℂ) 2
have h₁ : (↑Var[HSMul.hSMul (β := (a : E) → ℝ) u (⇑L : (a : E) → ℝ); μ] : ℂ) =
  (↑Var[fun (ω : E) ↦ HMul.hMul (β := ℝ) u ((L : (a : E) → ℝ) ω : ℝ); μ] : ℂ)
Tactic: rw [max_eq_left (variance_nonneg _ _), mul_comm, ← ofReal_pow, ← ofReal_mul,
      ← variance_const_mul]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Basic (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
μ : Measure E
inst_4 : IsGaussian μ
t : E
⊢ charFun μ t = cexp ((∫ (x : E), (↑((fun (x : E) ↦ ⟪t, x⟫) x) : ℂ) ∂μ) * I - (↑Var[fun (x : E) ↦ ⟪t, x⟫; μ] : ℂ) / 2)
have rw : cexp
    ((∫ (x : E), (↑((((toDualMap ℝ E : (a : E) → StrongDual ℝ E) t : StrongDual ℝ E) : (a : E) → ℝ) x) : ℂ) ∂μ) * I -
      (↑Var[(⇑((toDualMap ℝ E : (a : E) → StrongDual ℝ E) t : StrongDual ℝ E) : (a : E) → ℝ); μ] : ℂ) / 2) =
  cexp ((∫ (x : E), (↑((fun (x : E) ↦ ⟪t, x⟫) x) : ℂ) ∂μ) * I - (↑Var[fun (x : E) ↦ ⟪t, x⟫; μ] : ℂ) / 2)
Tactic: rw [charFun_eq_charFunDual_toDualMap, IsGaussian.charFunDual_eq]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Basic (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
μ : Measure E
inst_4 : CompleteSpace E
inst_5 : IsFiniteMeasure μ
⊢ IsGaussian μ ↔
    ∀ (t : E),
      charFun μ t =
        cexp ((∫ (x : E), (↑((fun (x : E) ↦ ⟪t, x⟫) x) : ℂ) ∂μ) * I - (↑Var[fun (x : E) ↦ ⟪t, x⟫; μ] : ℂ) / 2)
have simp_rw : (∀ (x : E),
    charFunDual μ ((toDual ℝ E : (a : E) → StrongDual ℝ E) x) =
      cexp
        ((∫ (x_1 : E), (↑((((toDual ℝ E : (a : E) → StrongDual ℝ E) x : StrongDual ℝ E) : (a : E) → ℝ) x_1) : ℂ) ∂μ) *
            I -
          (↑Var[(⇑((toDual ℝ E : (a : E) → StrongDual ℝ E) x : StrongDual ℝ E) : (a : E) → ℝ); μ] : ℂ) / 2)) ↔
  ∀ (t : E),
    charFunDual μ ((toDualMap ℝ E : (a : E) → StrongDual ℝ E) t) =
      cexp ((∫ (x : E), (↑⟪t, x⟫ : ℂ) ∂μ) * I - (↑Var[fun (x : E) ↦ ⟪t, x⟫; μ] : ℂ) / 2)
Tactic: simp_rw [isGaussian_iff_charFunDual_eq, (toDual ℝ E).surjective.forall,
    charFun_eq_charFunDual_toDualMap]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Basic (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ_1 : Measure E
inst_8 : IsGaussian μ_1
inst_9 : SecondCountableTopology E
μ ν : Measure E
inst_10 : IsGaussian μ
inst_11 : IsGaussian ν
L : StrongDual ℝ E
⊢ Eq (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ ∗ ν)
    (@integral _ _ _ _ Real.measurableSpace (Measure.map (⇑L : (a : E) → ℝ) μ ∗ Measure.map (⇑L : (a : E) → ℝ) ν)
      fun (x : ℝ) ↦ x)
have rw : Eq (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ ∗ ν)
  (@integral _ _ _ _ Real.measurableSpace (Measure.map (⇑L : (a : E) → ℝ) (μ ∗ ν)) fun (x : ℝ) ↦ x)
Tactic: rw [← Measure.map_conv_continuousLinearMap L,
        integral_map (φ := L) (by fun_prop) (by fun_prop)]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Basic (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ_1 : Measure E
inst_8 : IsGaussian μ_1
inst_9 : SecondCountableTopology E
μ ν : Measure E
inst_10 : IsGaussian μ
inst_11 : IsGaussian ν
L : StrongDual ℝ E
rw :
  Eq (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ ∗ ν)
    (@integral _ _ _ _ Real.measurableSpace (Measure.map (⇑L : (a : E) → ℝ) (μ ∗ ν)) fun (x : ℝ) ↦ x)
⊢ Eq (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ ∗ ν)
    (@integral _ _ _ _ Real.measurableSpace (Measure.map (⇑L : (a : E) → ℝ) μ ∗ Measure.map (⇑L : (a : E) → ℝ) ν)
      fun (x : ℝ) ↦ x)
have rw₁ : Eq (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ ∗ ν) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ ∗ ν)
Tactic: rw [← Measure.map_conv_continuousLinearMap L,
        integral_map (φ := L) (by fun_prop) (by fun_prop)]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Basic (hypothesis)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ_1 : Measure E
inst_8 : IsGaussian μ_1
inst_9 : SecondCountableTopology E
μ ν : Measure E
inst_10 : IsGaussian μ
inst_11 : IsGaussian ν
L : StrongDual ℝ E
⊢ Measure.map (⇑L : (a : E) → ℝ) (μ ∗ ν) =
    gaussianReal (∫ (x : E), (L : (a : E) → ℝ) x ∂μ ∗ ν) Var[(⇑L : (a : E) → ℝ); μ ∗ ν].toNNReal
have this : Eq (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ ∗ ν)
  (@integral _ _ _ _ Real.measurableSpace (Measure.map (⇑L : (a : E) → ℝ) μ ∗ Measure.map (⇑L : (a : E) → ℝ) ν)
    fun (x : ℝ) ↦ x)
Tactic: have : (μ ∗ ν)[L] = ∫ x, x ∂((μ.map L).conv (ν.map L)) := by
      rw [← Measure.map_conv_continuousLinearMap L,
        integral_map (φ := L) (by fun_prop) (by fun_prop)]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Basic (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ_1 : Measure E
inst_8 : IsGaussian μ_1
inst_9 : SecondCountableTopology E
μ ν : Measure E
inst_10 : IsGaussian μ
inst_11 : IsGaussian ν
L : StrongDual ℝ E
this :
  Eq (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ ∗ ν)
    (@integral _ _ _ _ Real.measurableSpace (Measure.map (⇑L : (a : E) → ℝ) μ ∗ Measure.map (⇑L : (a : E) → ℝ) ν)
      fun (x : ℝ) ↦ x)
⊢ Measure.map (⇑L : (a : E) → ℝ) (μ ∗ ν) =
    gaussianReal (∫ (x : E), (L : (a : E) → ℝ) x ∂μ ∗ ν) Var[(⇑L : (a : E) → ℝ); μ ∗ ν].toNNReal
have rw : gaussianReal (HAdd.hAdd (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ) (∫ (x : E), (L : (a : E) → ℝ) x ∂ν))
    (Var[(⇑L : (a : E) → ℝ); μ].toNNReal + Var[(⇑L : (a : E) → ℝ); ν].toNNReal) =
  gaussianReal
    (∫ (x : ℝ),
      x ∂gaussianReal (HAdd.hAdd (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ) (∫ (x : E), (L : (a : E) → ℝ) x ∂ν))
        (Var[(⇑L : (a : E) → ℝ); μ].toNNReal + Var[(⇑L : (a : E) → ℝ); ν].toNNReal))
    Var[id;
        gaussianReal (HAdd.hAdd (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ) (∫ (x : E), (L : (a : E) → ℝ) x ∂ν))
          (Var[(⇑L : (a : E) → ℝ); μ].toNNReal + Var[(⇑L : (a : E) → ℝ); ν].toNNReal)].toNNReal
Tactic: rw [Measure.map_conv_continuousLinearMap L, this, ← variance_id_map (by fun_prop),
      Measure.map_conv_continuousLinearMap L, IsGaussian.map_eq_gaussianReal L,
      IsGaussian.map_eq_gaussianReal L, gaussianReal_conv_gaussianReal]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Basic (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ_1 : Measure E
inst_8 : IsGaussian μ_1
inst_9 : SecondCountableTopology E
μ ν : Measure E
inst_10 : IsGaussian μ
inst_11 : IsGaussian ν
L : StrongDual ℝ E
this :
  Eq (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ ∗ ν)
    (@integral _ _ _ _ Real.measurableSpace (Measure.map (⇑L : (a : E) → ℝ) μ ∗ Measure.map (⇑L : (a : E) → ℝ) ν)
      fun (x : ℝ) ↦ x)
⊢ gaussianReal (HAdd.hAdd (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ) (∫ (x : E), (L : (a : E) → ℝ) x ∂ν))
      (Var[(⇑L : (a : E) → ℝ); μ].toNNReal + Var[(⇑L : (a : E) → ℝ); ν].toNNReal) =
    gaussianReal
      (∫ (x : ℝ),
        x ∂gaussianReal (HAdd.hAdd (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ) (∫ (x : E), (L : (a : E) → ℝ) x ∂ν))
          (Var[(⇑L : (a : E) → ℝ); μ].toNNReal + Var[(⇑L : (a : E) → ℝ); ν].toNNReal))
      Var[id;
          gaussianReal (HAdd.hAdd (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ) (∫ (x : E), (L : (a : E) → ℝ) x ∂ν))
            (Var[(⇑L : (a : E) → ℝ); μ].toNNReal + Var[(⇑L : (a : E) → ℝ); ν].toNNReal)].toNNReal
have e_μ : HAdd.hAdd (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ) (∫ (x : E), (L : (a : E) → ℝ) x ∂ν) =
  ∫ (x : ℝ),
    x ∂gaussianReal (HAdd.hAdd (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ) (∫ (x : E), (L : (a : E) → ℝ) x ∂ν))
      (Var[(⇑L : (a : E) → ℝ); μ].toNNReal + Var[(⇑L : (a : E) → ℝ); ν].toNNReal)
Tactic: congr
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Basic (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ_1 : Measure E
inst_8 : IsGaussian μ_1
inst_9 : SecondCountableTopology E
μ ν : Measure E
inst_10 : IsGaussian μ
inst_11 : IsGaussian ν
L : StrongDual ℝ E
this :
  Eq (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ ∗ ν)
    (@integral _ _ _ _ Real.measurableSpace (Measure.map (⇑L : (a : E) → ℝ) μ ∗ Measure.map (⇑L : (a : E) → ℝ) ν)
      fun (x : ℝ) ↦ x)
e_μ :
  HAdd.hAdd (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ) (∫ (x : E), (L : (a : E) → ℝ) x ∂ν) =
    ∫ (x : ℝ),
      x ∂gaussianReal (HAdd.hAdd (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ) (∫ (x : E), (L : (a : E) → ℝ) x ∂ν))
        (Var[(⇑L : (a : E) → ℝ); μ].toNNReal + Var[(⇑L : (a : E) → ℝ); ν].toNNReal)
⊢ gaussianReal (HAdd.hAdd (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ) (∫ (x : E), (L : (a : E) → ℝ) x ∂ν))
      (Var[(⇑L : (a : E) → ℝ); μ].toNNReal + Var[(⇑L : (a : E) → ℝ); ν].toNNReal) =
    gaussianReal
      (∫ (x : ℝ),
        x ∂gaussianReal (HAdd.hAdd (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ) (∫ (x : E), (L : (a : E) → ℝ) x ∂ν))
          (Var[(⇑L : (a : E) → ℝ); μ].toNNReal + Var[(⇑L : (a : E) → ℝ); ν].toNNReal))
      Var[id;
          gaussianReal (HAdd.hAdd (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ) (∫ (x : E), (L : (a : E) → ℝ) x ∂ν))
            (Var[(⇑L : (a : E) → ℝ); μ].toNNReal + Var[(⇑L : (a : E) → ℝ); ν].toNNReal)].toNNReal
have e_v : Var[(⇑L : (a : E) → ℝ); μ].toNNReal + Var[(⇑L : (a : E) → ℝ); ν].toNNReal =
  Var[id;
      gaussianReal (HAdd.hAdd (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ) (∫ (x : E), (L : (a : E) → ℝ) x ∂ν))
        (Var[(⇑L : (a : E) → ℝ); μ].toNNReal + Var[(⇑L : (a : E) → ℝ); ν].toNNReal)].toNNReal
Tactic: congr
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Basic (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure E
inst_8 : IsGaussian μ
c : E
⊢ IsGaussian (E := E) (mE := inst_2) (Measure.map (fun (x : E) ↦ x + c) μ)
have refine : ∀ (L : StrongDual ℝ E),
  charFunDual (mE := inst_2) (Measure.map (fun (x : E) ↦ x + c) μ) L =
    cexp
      ((@integral _ _ _ _ inst_2 (Measure.map (fun (x : E) ↦ x + c) μ) fun (x : E) ↦ (↑((L : (a : E) → ℝ) x) : ℂ)) * I -
        (↑(variance (Ω := E) (mΩ := inst_2) (⇑L : (a : E) → ℝ) (Measure.map (fun (x : E) ↦ x + c) μ)) : ℂ) / 2)
Tactic: refine isGaussian_of_charFunDual_eq fun L ↦ ?_
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Basic (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure E
inst_8 : IsGaussian μ
c : E
L : StrongDual ℝ E
⊢ charFunDual (mE := inst_2) (Measure.map (fun (x : E) ↦ x + c) μ) L =
    cexp
      ((@integral _ _ _ _ inst_2 (Measure.map (fun (x : E) ↦ x + c) μ) fun (x : E) ↦ (↑((L : (a : E) → ℝ) x) : ℂ)) * I -
        (↑(variance (Ω := E) (mΩ := inst_2) (⇑L : (a : E) → ℝ) (Measure.map (fun (x : E) ↦ x + c) μ)) : ℂ) / 2)
have rw : cexp
    ((∫ (x : E), (↑((L : (a : E) → ℝ) x) : ℂ) ∂μ) * I - (↑Var[(⇑L : (a : E) → ℝ); μ] : ℂ) / 2 +
      (↑((L : (a : E) → ℝ) c) : ℂ) * I) =
  cexp
    ((@integral _ _ _ _ inst_2 (Measure.map (fun (x : E) ↦ x + c) μ) fun (x : E) ↦ (↑((L : (a : E) → ℝ) x) : ℂ)) * I -
      (↑(variance (Ω := E) (mΩ := inst_2) (⇑L : (a : E) → ℝ) (Measure.map (fun (x : E) ↦ x + c) μ)) : ℂ) / 2)
Tactic: rw [charFunDual_map_add_const, IsGaussian.charFunDual_eq, ← exp_add]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Basic (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure E
inst_8 : IsGaussian μ
c : E
L : StrongDual ℝ E
⊢ Eq (α := E → ℝ) (Function.comp (β := E) (⇑L : (a : E) → ℝ) fun (x : E) ↦ x + c) fun (x : E) ↦
    HAdd.hAdd (α := ℝ) (β := ℝ) ((L : (a : E) → ℝ) x : ℝ) ((L : (a : E) → ℝ) c : ℝ)
have h : ∀ (x : E),
  Function.comp (β := E) (⇑L : (a : E) → ℝ) (fun (x : E) ↦ x + c) x =
    HAdd.hAdd (α := ℝ) (β := ℝ) ((L : (a : E) → ℝ) x : ℝ) ((L : (a : E) → ℝ) c : ℝ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Basic (hypothesis)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure E
inst_8 : IsGaussian μ
c : E
L : StrongDual ℝ E
⊢ cexp
      ((∫ (x : E), (↑((L : (a : E) → ℝ) x) : ℂ) ∂μ) * I - (↑Var[(⇑L : (a : E) → ℝ); μ] : ℂ) / 2 +
        (↑((L : (a : E) → ℝ) c) : ℂ) * I) =
    cexp
      ((@integral _ _ _ _ inst_2 (Measure.map (fun (x : E) ↦ x + c) μ) fun (x : E) ↦ (↑((L : (a : E) → ℝ) x) : ℂ)) * I -
        (↑(variance (Ω := E) (mΩ := inst_2) (⇑L : (a : E) → ℝ) (Measure.map (fun (x : E) ↦ x + c) μ)) : ℂ) / 2)
have hL_comp : Eq (α := E → ℝ) (Function.comp (β := E) (⇑L : (a : E) → ℝ) fun (x : E) ↦ x + c) fun (x : E) ↦
  HAdd.hAdd (α := ℝ) (β := ℝ) ((L : (a : E) → ℝ) x : ℝ) ((L : (a : E) → ℝ) c : ℝ)
Tactic: have hL_comp : L ∘ (fun x ↦ x + c) = fun x ↦ L x + L c := by ext; simp
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Basic (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure E
inst_8 : IsGaussian μ
c : E
L : StrongDual ℝ E
hL_comp :
  Eq (α := E → ℝ) (Function.comp (β := E) (⇑L : (a : E) → ℝ) fun (x : E) ↦ x + c) fun (x : E) ↦
    HAdd.hAdd (α := ℝ) (β := ℝ) ((L : (a : E) → ℝ) x : ℝ) ((L : (a : E) → ℝ) c : ℝ)
⊢ cexp
      ((∫ (x : E), (↑((L : (a : E) → ℝ) x) : ℂ) ∂μ) * I - (↑Var[(⇑L : (a : E) → ℝ); μ] : ℂ) / 2 +
        (↑((L : (a : E) → ℝ) c) : ℂ) * I) =
    cexp
      ((@integral _ _ _ _ inst_2 (Measure.map (fun (x : E) ↦ x + c) μ) fun (x : E) ↦ (↑((L : (a : E) → ℝ) x) : ℂ)) * I -
        (↑(variance (Ω := E) (mΩ := inst_2) (⇑L : (a : E) → ℝ) (Measure.map (fun (x : E) ↦ x + c) μ)) : ℂ) / 2)
have rw : cexp
    ((↑(∫ (x : E), (L : (a : E) → ℝ) x ∂μ) : ℂ) * I - (↑Var[(⇑L : (a : E) → ℝ); μ] : ℂ) / 2 +
      (↑((L : (a : E) → ℝ) c) : ℂ) * I) =
  cexp ((↑(∫ (x : E), (L : (a : E) → ℝ) (x + c) ∂μ) : ℂ) * I - (↑Var[(⇑L : (a : E) → ℝ); μ] : ℂ) / 2)
Tactic: rw [variance_map (by fun_prop) (by fun_prop), integral_map (by fun_prop) (by fun_prop),
    hL_comp, variance_add_const (by fun_prop), integral_complex_ofReal, integral_complex_ofReal]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Basic (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure E
inst_8 : IsGaussian μ
c : E
L : StrongDual ℝ E
hL_comp :
  Eq (α := E → ℝ) (Function.comp (β := E) (⇑L : (a : E) → ℝ) fun (x : E) ↦ x + c) fun (x : E) ↦
    HAdd.hAdd (α := ℝ) (β := ℝ) ((L : (a : E) → ℝ) x : ℝ) ((L : (a : E) → ℝ) c : ℝ)
⊢ cexp
      ((↑(∫ (x : E), (L : (a : E) → ℝ) x ∂μ) : ℂ) * I - (↑Var[(⇑L : (a : E) → ℝ); μ] : ℂ) / 2 +
        (↑((L : (a : E) → ℝ) c) : ℂ) * I) =
    cexp ((↑(∫ (x : E), (L : (a : E) → ℝ) (x + c) ∂μ) : ℂ) * I - (↑Var[(⇑L : (a : E) → ℝ); μ] : ℂ) / 2)
have simp : cexp
    ((↑(∫ (x : E), (L : (a : E) → ℝ) x ∂μ) : ℂ) * I - (↑Var[(⇑L : (a : E) → ℝ); μ] : ℂ) / 2 +
      (↑((L : (a : E) → ℝ) c) : ℂ) * I) =
  cexp
    ((↑(∫ (x : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((L : (a : E) → ℝ) x : ℝ) ((L : (a : E) → ℝ) c : ℝ) ∂μ) : ℂ) * I -
      (↑Var[(⇑L : (a : E) → ℝ); μ] : ℂ) / 2)
Tactic: simp only [map_add]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Basic (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure E
inst_8 : IsGaussian μ
c : E
L : StrongDual ℝ E
hL_comp :
  Eq (α := E → ℝ) (Function.comp (β := E) (⇑L : (a : E) → ℝ) fun (x : E) ↦ x + c) fun (x : E) ↦
    HAdd.hAdd (α := ℝ) (β := ℝ) ((L : (a : E) → ℝ) x : ℝ) ((L : (a : E) → ℝ) c : ℝ)
⊢ Integrable (ε := ℝ) (fun (x : E) ↦ (L : (a : E) → ℝ) c) μ
have funProp : enorm (E := ℝ) ((L : (a : E) → ℝ) c : ℝ) ≠ ∞
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Basic (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure E
inst_8 : IsGaussian μ
c : E
L : StrongDual ℝ E
hL_comp :
  Eq (α := E → ℝ) (Function.comp (β := E) (⇑L : (a : E) → ℝ) fun (x : E) ↦ x + c) fun (x : E) ↦
    HAdd.hAdd (α := ℝ) (β := ℝ) ((L : (a : E) → ℝ) x : ℝ) ((L : (a : E) → ℝ) c : ℝ)
⊢ cexp
      ((↑(∫ (x : E), (L : (a : E) → ℝ) x ∂μ) : ℂ) * I - (↑Var[(⇑L : (a : E) → ℝ); μ] : ℂ) / 2 +
        (↑((L : (a : E) → ℝ) c) : ℂ) * I) =
    cexp
      ((↑(∫ (x : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((L : (a : E) → ℝ) x : ℝ) ((L : (a : E) → ℝ) c : ℝ) ∂μ) : ℂ) * I -
        (↑Var[(⇑L : (a : E) → ℝ); μ] : ℂ) / 2)
have rw : cexp
    ((↑(∫ (x : E), (L : (a : E) → ℝ) x ∂μ) : ℂ) * I - (↑Var[(⇑L : (a : E) → ℝ); μ] : ℂ) / 2 +
      (↑((L : (a : E) → ℝ) c) : ℂ) * I) =
  cexp
    ((↑(HAdd.hAdd (α := ℝ) (∫ (a : E), (L : (a : E) → ℝ) a ∂μ) (∫ (a : E), (L : (a : E) → ℝ) c ∂μ)) : ℂ) * I -
      (↑Var[(⇑L : (a : E) → ℝ); μ] : ℂ) / 2)
Tactic: rw [integral_add (by fun_prop) (by fun_prop)]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Basic (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure E
inst_8 : IsGaussian μ
c : E
L : StrongDual ℝ E
hL_comp :
  Eq (α := E → ℝ) (Function.comp (β := E) (⇑L : (a : E) → ℝ) fun (x : E) ↦ x + c) fun (x : E) ↦
    HAdd.hAdd (α := ℝ) (β := ℝ) ((L : (a : E) → ℝ) x : ℝ) ((L : (a : E) → ℝ) c : ℝ)
⊢ cexp
      ((↑(∫ (x : E), (L : (a : E) → ℝ) x ∂μ) : ℂ) * I - (↑Var[(⇑L : (a : E) → ℝ); μ] : ℂ) / 2 +
        (↑((L : (a : E) → ℝ) c) : ℂ) * I) =
    cexp
      ((↑(HAdd.hAdd (α := ℝ) (∫ (a : E), (L : (a : E) → ℝ) a ∂μ) (∫ (a : E), (L : (a : E) → ℝ) c ∂μ)) : ℂ) * I -
        (↑Var[(⇑L : (a : E) → ℝ); μ] : ℂ) / 2)
have e_z : (↑(∫ (x : E), (L : (a : E) → ℝ) x ∂μ) : ℂ) * I - (↑Var[(⇑L : (a : E) → ℝ); μ] : ℂ) / 2 +
    (↑((L : (a : E) → ℝ) c) : ℂ) * I =
  (↑(HAdd.hAdd (α := ℝ) (∫ (a : E), (L : (a : E) → ℝ) a ∂μ) (∫ (a : E), (L : (a : E) → ℝ) c ∂μ)) : ℂ) * I -
    (↑Var[(⇑L : (a : E) → ℝ); μ] : ℂ) / 2
Tactic: congr
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Basic (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure E
inst_8 : IsGaussian μ
c : E
L : StrongDual ℝ E
hL_comp :
  Eq (α := E → ℝ) (Function.comp (β := E) (⇑L : (a : E) → ℝ) fun (x : E) ↦ x + c) fun (x : E) ↦
    HAdd.hAdd (α := ℝ) (β := ℝ) ((L : (a : E) → ℝ) x : ℝ) ((L : (a : E) → ℝ) c : ℝ)
⊢ (↑(∫ (x : E), (L : (a : E) → ℝ) x ∂μ) : ℂ) * I - (↑Var[(⇑L : (a : E) → ℝ); μ] : ℂ) / 2 +
      (↑((L : (a : E) → ℝ) c) : ℂ) * I =
    (↑(HAdd.hAdd (α := ℝ) (∫ (a : E), (L : (a : E) → ℝ) a ∂μ) (∫ (a : E), (L : (a : E) → ℝ) c ∂μ)) : ℂ) * I -
      (↑Var[(⇑L : (a : E) → ℝ); μ] : ℂ) / 2
have e_z : (↑(∫ (x : E), (L : (a : E) → ℝ) x ∂μ) : ℂ) * I - (↑Var[(⇑L : (a : E) → ℝ); μ] : ℂ) / 2 +
    (↑((L : (a : E) → ℝ) c) : ℂ) * I =
  ((↑(∫ (x : E), (L : (a : E) → ℝ) x ∂μ) : ℂ) + (↑((L : (a : E) → ℝ) c) : ℂ)) * I -
    (↑Var[(⇑L : (a : E) → ℝ); μ] : ℂ) / 2
Tactic: simp only [integral_const, probReal_univ, smul_eq_mul, one_mul, ofReal_add]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Basic (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure E
inst_8 : IsGaussian μ
c : E
⊢ IsGaussian (E := E) (mE := inst_2) (Measure.map (fun (x : E) ↦ c + x) μ)
have simp_rw : IsGaussian (E := E) (mE := inst_2) (Measure.map (fun (x : E) ↦ x + c) μ)
Tactic: simp_rw [add_comm c]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Basic (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure E
inst_8 : IsGaussian μ
c : E
⊢ IsGaussian (E := E) (mE := inst_2) (Measure.map (fun (x : E) ↦ x - c) μ)
have simp_rw : IsGaussian (E := E) (mE := inst_2) (Measure.map (fun (x : E) ↦ x + -c) μ)
Tactic: simp_rw [sub_eq_add_neg]