awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Basic (goal)
Goal:
E : Type u_1
F : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommMonoid E
inst_2 : Module ℝ E
mE : MeasurableSpace E
inst_3 : TopologicalSpace F
inst_4 : AddCommMonoid F
inst_5 : Module ℝ F
mF : MeasurableSpace F
inst_6 : OpensMeasurableSpace F
μ : Measure E
L : E →L[ℝ] F
inst_7 : IsGaussian μ
hL : Measurable.{u_1, u_2} (α := E) (β := F) (⇑L : (a : E) → F)
L' : F →L[ℝ] ℝ
rw :
  Measure.map (Function.comp (β := F) (⇑L' : (a : F) → ℝ) (⇑L : (a : E) → F)) μ =
    gaussianReal (∫ (x : E), (L' ∘SL L : (a : E) → ℝ) x ∂μ) Var[(⇑(L' ∘SL L) : (a : E) → ℝ); μ].toNNReal
rw₁ :
  Measure.map (⇑(L' ∘SL L) : (a : E) → ℝ) μ =
    gaussianReal (∫ (x : E), (L' ∘SL L : (a : E) → ℝ) x ∂μ) Var[(⇑(L' ∘SL L) : (a : E) → ℝ); μ].toNNReal
⊢ Measure.map (α := F) (⇑L' : (a : F) → ℝ) (Measure.map (⇑L : (a : E) → F) μ) =
    gaussianReal (∫ (x : E), (L' ∘SL L : (a : E) → ℝ) x ∂μ) Var[(⇑(L' ∘SL L) : (a : E) → ℝ); μ].toNNReal
have rw₂ : gaussianReal (∫ (x : E), (L' ∘SL L : (a : E) → ℝ) x ∂μ) Var[(⇑(L' ∘SL L) : (a : E) → ℝ); μ].toNNReal =
  gaussianReal (∫ (x : E), (L' ∘SL L : (a : E) → ℝ) x ∂μ) Var[(⇑(L' ∘SL L) : (a : E) → ℝ); μ].toNNReal
Tactic: rw [Measure.map_map (by fun_prop) hL, ← ContinuousLinearMap.coe_comp',
    IsGaussian.map_eq_gaussianReal]
-- 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 : Subsingleton E
inst_5 : IsProbabilityMeasure μ
⊢ IsGaussian μ
have h : μ = Measure.dirac 0
Tactic: convert! instIsGaussianDirac (x := (0 : E))
-- 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 : Subsingleton E
inst_5 : IsProbabilityMeasure μ
⊢ μ = Measure.dirac 0
have h : ∀ (s : Set E),
  Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (((Measure.dirac 0 : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext s -
-- 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 : Subsingleton E
inst_5 : IsProbabilityMeasure μ
s : Set E
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (((Measure.dirac 0 : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
have h : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) ∅ : ℝ≥0∞) (((Measure.dirac 0 : Measure E) : (a : Set E) → ℝ≥0∞) ∅ : ℝ≥0∞)
Tactic: apply Subsingleton.set_cases (p := fun s ↦ μ s = _)
-- 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 : Subsingleton E
inst_5 : IsProbabilityMeasure μ
s : Set E
h : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) ∅ : ℝ≥0∞) (((Measure.dirac 0 : Measure E) : (a : Set E) → ℝ≥0∞) ∅ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (((Measure.dirac 0 : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
have h₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) Set.univ : ℝ≥0∞)
  (((Measure.dirac 0 : Measure E) : (a : Set E) → ℝ≥0∞) Set.univ : ℝ≥0∞)
Tactic: apply Subsingleton.set_cases (p := fun s ↦ μ s = _)
-- 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 : IsGaussian μ
L : StrongDual ℝ E
p : ℝ≥0∞
hp : p ≠ ∞
⊢ MemLp (ε := ℝ) (id ∘ (⇑L : (a : E) → ℝ)) p μ
have rw : MemLp id p (gaussianReal (∫ (x : E), (L : (a : E) → ℝ) x ∂μ) Var[(⇑L : (a : E) → ℝ); μ].toNNReal)
Tactic: rw [← memLp_map_measure_iff (by fun_prop) (by fun_prop), IsGaussian.map_eq_gaussianReal L]
-- 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 : IsGaussian μ
L : StrongDual ℝ E
p : ℝ≥0∞
hp : p ≠ ∞
⊢ MemLp id p (gaussianReal (∫ (x : E), (L : (a : E) → ℝ) x ∂μ) Var[(⇑L : (a : E) → ℝ); μ].toNNReal)
have h : p = (↑p.toNNReal : ℝ≥0∞)
Tactic: convert! memLp_id_gaussianReal p.toNNReal
-- 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 : IsGaussian μ
L : StrongDual ℝ E
⊢ Integrable (ε := ℝ) (⇑L : (a : E) → ℝ) μ
have rw : MemLp (ε := ℝ) (⇑L : (a : E) → ℝ) 1 μ
Tactic: rw [← memLp_one_iff_integrable]
-- 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
L : E ≃L[ℝ] F
⊢ IsGaussian.{u_2} (E := F) (mE := inst_6) (Measure.map (⇑L : (a : E) → F) μ) ↔ IsGaussian μ
have refine : ∀ (h : IsGaussian.{u_2} (E := F) (mE := inst_6) (Measure.map (⇑L : (a : E) → F) μ)), IsGaussian μ
Tactic: refine ⟨fun h ↦ ?_, fun _ ↦ inferInstance⟩
-- 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
L : E ≃L[ℝ] F
h : IsGaussian.{u_2} (E := F) (mE := inst_6) (Measure.map (⇑L : (a : E) → F) μ)
this : μ = Measure.map.{u_2, u_1} (α := F) (⇑L.symm : (a : F) → E) (Measure.map (⇑L : (a : E) → F) μ)
⊢ IsGaussian μ
have rw : IsGaussian.{u_1} (E := E) (mE := inst_2)
  (Measure.map.{u_2, u_1} (α := F) (⇑L.symm : (a : F) → E) (Measure.map (⇑L : (a : E) → F) μ))
Tactic: rw [this]
-- 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
L : E ≃L[ℝ] F
h : IsGaussian.{u_2} (E := F) (mE := inst_6) (Measure.map (⇑L : (a : E) → F) μ)
⊢ IsGaussian μ
have suffices : μ = Measure.map.{u_2, u_1} (α := F) (⇑L.symm : (a : F) → E) (Measure.map (⇑L : (a : E) → F) μ)
Tactic: suffices μ = (μ.map L).map L.symm by rw [this]; infer_instance
-- 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
L : E ≃L[ℝ] F
h : IsGaussian.{u_2} (E := F) (mE := inst_6) (Measure.map (⇑L : (a : E) → F) μ)
⊢ Measurable.{u_2, u_1} (α := F) (β := E) (⇑L.symm : (a : F) → E)
have funProp : inst_6 ≤ inst_6
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
L : E ≃L[ℝ] F
h : IsGaussian.{u_2} (E := F) (mE := inst_6) (Measure.map (⇑L : (a : E) → F) μ)
funProp : inst_6 ≤ inst_6
⊢ Measurable.{u_2, u_1} (α := F) (β := E) (⇑L.symm : (a : F) → E)
have funProp₁ : MeasurableEmbedding.{u_2, u_1} (β := E) fun (a : F) ↦ (L.symm : (a : F) → E) a
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
L : E ≃L[ℝ] F
h : IsGaussian.{u_2} (E := F) (mE := inst_6) (Measure.map (⇑L : (a : E) → F) μ)
⊢ Measurable.{u_1, u_2} (α := E) (β := F) (⇑L : (a : E) → F)
have funProp : inst_2 ≤ inst_2
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
L : E ≃L[ℝ] F
h : IsGaussian.{u_2} (E := F) (mE := inst_6) (Measure.map (⇑L : (a : E) → F) μ)
funProp : inst_2 ≤ inst_2
⊢ Measurable.{u_1, u_2} (α := E) (β := F) (⇑L : (a : E) → F)
have funProp₁ : MeasurableEmbedding.{u_1, u_2} (β := F) fun (a : E) ↦ (L : (a : E) → F) a
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
L : E ≃L[ℝ] F
h : IsGaussian.{u_2} (E := F) (mE := inst_6) (Measure.map (⇑L : (a : E) → F) μ)
⊢ μ = Measure.map.{u_2, u_1} (α := F) (⇑L.symm : (a : F) → E) (Measure.map (⇑L : (a : E) → F) μ)
have rw : μ = Measure.map (Function.comp.{u_1 + 1, u_2 + 1, u_1 + 1} (β := F) (⇑L.symm : (a : F) → E) (⇑L : (a : E) → F)) μ
Tactic: rw [Measure.map_map (by fun_prop) (by fun_prop)]
-- 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 : IsGaussian μ
L : StrongDual ℝ E
⊢ charFunDual μ L = charFun (E := ℝ) (mE := Real.measurableSpace) (Measure.map (⇑L : (a : E) → ℝ) μ) 1
have rw : charFun (E := ℝ) (mE := Real.measurableSpace) (Measure.map (⇑L : (a : E) → ℝ) μ) 1 =
  charFun (E := ℝ) (mE := Real.measurableSpace) (Measure.map (⇑L : (a : E) → ℝ) μ) 1
Tactic: rw [charFunDual_eq_charFun_map_one]
-- 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 : IsGaussian μ
L : StrongDual ℝ E
⊢ charFun (E := ℝ) (mE := Real.measurableSpace) (Measure.map (⇑L : (a : E) → ℝ) μ) 1 =
    charFun (gaussianReal (∫ (x : E), (L : (a : E) → ℝ) x ∂μ) Var[(⇑L : (a : E) → ℝ); μ].toNNReal) 1
have rw : charFun (gaussianReal (∫ (x : E), (L : (a : E) → ℝ) x ∂μ) Var[(⇑L : (a : E) → ℝ); μ].toNNReal) 1 =
  charFun (gaussianReal (∫ (x : E), (L : (a : E) → ℝ) x ∂μ) Var[(⇑L : (a : E) → ℝ); μ].toNNReal) 1
Tactic: rw [IsGaussian.map_eq_gaussianReal L]
-- 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 : IsGaussian μ
L : StrongDual ℝ E
⊢ charFun (gaussianReal (∫ (x : E), (L : (a : E) → ℝ) x ∂μ) Var[(⇑L : (a : E) → ℝ); μ].toNNReal) 1 =
    cexp ((∫ (x : E), (↑((L : (a : E) → ℝ) x) : ℂ) ∂μ) * I - (↑Var[(⇑L : (a : E) → ℝ); μ] : ℂ) / 2)
have rw : cexp
    ((↑1 : ℂ) * (↑(∫ (x : E), (L : (a : E) → ℝ) x ∂μ) : ℂ) * I -
      (↑(↑Var[(⇑L : (a : E) → ℝ); μ].toNNReal : ℝ) : ℂ) * HPow.hPow (β := ℕ) (↑1 : ℂ) 2 / 2) =
  cexp ((∫ (x : E), (↑((L : (a : E) → ℝ) x) : ℂ) ∂μ) * I - (↑Var[(⇑L : (a : E) → ℝ); μ] : ℂ) / 2)
Tactic: rw [charFun_gaussianReal]
-- 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 : IsGaussian μ
L : StrongDual ℝ E
⊢ cexp
      ((↑1 : ℂ) * (↑(∫ (x : E), (L : (a : E) → ℝ) x ∂μ) : ℂ) * I -
        (↑(↑Var[(⇑L : (a : E) → ℝ); μ].toNNReal : ℝ) : ℂ) * HPow.hPow (β := ℕ) (↑1 : ℂ) 2 / 2) =
    cexp ((∫ (x : E), (↑((L : (a : E) → ℝ) x) : ℂ) ∂μ) * I - (↑Var[(⇑L : (a : E) → ℝ); μ] : ℂ) / 2)
have simp : cexp ((↑(∫ (x : E), (L : (a : E) → ℝ) x ∂μ) : ℂ) * I - (↑(max Var[(⇑L : (a : E) → ℝ); μ] 0) : ℂ) / 2) =
  cexp ((∫ (x : E), (↑((L : (a : E) → ℝ) x) : ℂ) ∂μ) * I - (↑Var[(⇑L : (a : E) → ℝ); μ] : ℂ) / 2)
Tactic: simp only [ofReal_one, one_mul, Real.coe_toNNReal', one_pow, mul_one]
-- 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 : IsGaussian μ
L : StrongDual ℝ E
⊢ cexp ((↑(∫ (x : E), (L : (a : E) → ℝ) x ∂μ) : ℂ) * I - (↑(max Var[(⇑L : (a : E) → ℝ); μ] 0) : ℂ) / 2) =
    cexp ((∫ (x : E), (↑((L : (a : E) → ℝ) x) : ℂ) ∂μ) * I - (↑Var[(⇑L : (a : E) → ℝ); μ] : ℂ) / 2)
have e_z : (↑(∫ (x : E), (L : (a : E) → ℝ) x ∂μ) : ℂ) = ∫ (x : E), (↑((L : (a : E) → ℝ) x) : ℂ) ∂μ
Tactic: congr
-- 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 : IsGaussian μ
L : StrongDual ℝ E
e_z : (↑(∫ (x : E), (L : (a : E) → ℝ) x ∂μ) : ℂ) = ∫ (x : E), (↑((L : (a : E) → ℝ) x) : ℂ) ∂μ
⊢ cexp ((↑(∫ (x : E), (L : (a : E) → ℝ) x ∂μ) : ℂ) * I - (↑(max Var[(⇑L : (a : E) → ℝ); μ] 0) : ℂ) / 2) =
    cexp ((∫ (x : E), (↑((L : (a : E) → ℝ) x) : ℂ) ∂μ) * I - (↑Var[(⇑L : (a : E) → ℝ); μ] : ℂ) / 2)
have e_z₁ : max Var[(⇑L : (a : E) → ℝ); μ] 0 = Var[(⇑L : (a : E) → ℝ); μ]
Tactic: congr
-- 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 : IsGaussian μ
L : StrongDual ℝ E
⊢ (↑(∫ (x : E), (L : (a : E) → ℝ) x ∂μ) : ℂ) = ∫ (x : E), (↑((L : (a : E) → ℝ) x) : ℂ) ∂μ
have e_z : (↑(∫ (x : E), (L : (a : E) → ℝ) x ∂μ) : ℂ) = (↑(∫ (x : E), (L : (a : E) → ℝ) x ∂μ) : ℂ)
Tactic: rw [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 : IsGaussian μ
L : StrongDual ℝ E
⊢ max Var[(⇑L : (a : E) → ℝ); μ] 0 = Var[(⇑L : (a : E) → ℝ); μ]
have e_z : 0 ≤ Var[(⇑L : (a : E) → ℝ); μ]
Tactic: simp only [sup_eq_left]
-- 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 : IsGaussian μ
L : StrongDual ℝ E
⊢ charFunDual μ L = cexp ((∫ (x : E), (↑((L : (a : E) → ℝ) x) : ℂ) ∂μ) * I - (↑Var[(⇑L : (a : E) → ℝ); μ] : ℂ) / 2)
have calc : charFunDual μ L = charFun (E := ℝ) (mE := Real.measurableSpace) (Measure.map (⇑L : (a : E) → ℝ) μ) 1
Tactic: calc charFunDual μ L
  _ = charFun (μ.map L) 1 := by rw [charFunDual_eq_charFun_map_one]
  _ = charFun (gaussianReal (μ[L]) (Var[L; μ]).toNNReal) 1 := by
    rw [IsGaussian.map_eq_gaussianReal L]
  _ = exp (μ[L] * I - Var[L; μ] / 2) := by
    rw [charFun_gaussianReal]
    simp only [ofReal_one, one_mul, Real.coe_toNNReal', one_pow, mul_one]
    congr
    · rw [integral_complex_ofReal]
    · simp only [sup_eq_left]
      exact variance_nonneg _ _
-- 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 : IsGaussian μ
L : StrongDual ℝ E
calc : charFunDual μ L = charFun (E := ℝ) (mE := Real.measurableSpace) (Measure.map (⇑L : (a : E) → ℝ) μ) 1
⊢ charFunDual μ L = cexp ((∫ (x : E), (↑((L : (a : E) → ℝ) x) : ℂ) ∂μ) * I - (↑Var[(⇑L : (a : E) → ℝ); μ] : ℂ) / 2)
have calc₁ : charFun (E := ℝ) (mE := Real.measurableSpace) (Measure.map (⇑L : (a : E) → ℝ) μ) 1 =
  charFun (gaussianReal (∫ (x : E), (L : (a : E) → ℝ) x ∂μ) Var[(⇑L : (a : E) → ℝ); μ].toNNReal) 1
Tactic: calc charFunDual μ L
  _ = charFun (μ.map L) 1 := by rw [charFunDual_eq_charFun_map_one]
  _ = charFun (gaussianReal (μ[L]) (Var[L; μ]).toNNReal) 1 := by
    rw [IsGaussian.map_eq_gaussianReal L]
  _ = exp (μ[L] * I - Var[L; μ] / 2) := by
    rw [charFun_gaussianReal]
    simp only [ofReal_one, one_mul, Real.coe_toNNReal', one_pow, mul_one]
    congr
    · rw [integral_complex_ofReal]
    · simp only [sup_eq_left]
      exact variance_nonneg _ _
-- 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 : IsGaussian μ
L : StrongDual ℝ E
calc : charFunDual μ L = charFun (E := ℝ) (mE := Real.measurableSpace) (Measure.map (⇑L : (a : E) → ℝ) μ) 1
calc₁ :
  charFun (E := ℝ) (mE := Real.measurableSpace) (Measure.map (⇑L : (a : E) → ℝ) μ) 1 =
    charFun (gaussianReal (∫ (x : E), (L : (a : E) → ℝ) x ∂μ) Var[(⇑L : (a : E) → ℝ); μ].toNNReal) 1
⊢ charFunDual μ L = cexp ((∫ (x : E), (↑((L : (a : E) → ℝ) x) : ℂ) ∂μ) * I - (↑Var[(⇑L : (a : E) → ℝ); μ] : ℂ) / 2)
have calc₂ : charFun (gaussianReal (∫ (x : E), (L : (a : E) → ℝ) x ∂μ) Var[(⇑L : (a : E) → ℝ); μ].toNNReal) 1 =
  cexp ((∫ (x : E), (↑((L : (a : E) → ℝ) x) : ℂ) ∂μ) * I - (↑Var[(⇑L : (a : E) → ℝ); μ] : ℂ) / 2)
Tactic: calc charFunDual μ L
  _ = charFun (μ.map L) 1 := by rw [charFunDual_eq_charFun_map_one]
  _ = charFun (gaussianReal (μ[L]) (Var[L; μ]).toNNReal) 1 := by
    rw [IsGaussian.map_eq_gaussianReal L]
  _ = exp (μ[L] * I - Var[L; μ] / 2) := by
    rw [charFun_gaussianReal]
    simp only [ofReal_one, one_mul, Real.coe_toNNReal', one_pow, mul_one]
    congr
    · rw [integral_complex_ofReal]
    · simp only [sup_eq_left]
      exact variance_nonneg _ _
-- 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 μ
⊢ IsGaussian μ ↔
    ∀ (L : StrongDual ℝ E),
      charFunDual μ L = cexp ((∫ (x : E), (↑((L : (a : E) → ℝ) x) : ℂ) ∂μ) * I - (↑Var[(⇑L : (a : E) → ℝ); μ] : ℂ) / 2)
have refine : ∀
  (h :
    ∀ (L : StrongDual ℝ E),
      charFunDual μ L = cexp ((∫ (x : E), (↑((L : (a : E) → ℝ) x) : ℂ) ∂μ) * I - (↑Var[(⇑L : (a : E) → ℝ); μ] : ℂ) / 2))
  (L : StrongDual ℝ E),
  charFun (mE := Real.measurableSpace) (Measure.map (⇑L : (a : E) → ℝ) μ) =
    charFun (gaussianReal (∫ (x : E), (L : (a : E) → ℝ) x ∂μ) Var[(⇑L : (a : E) → ℝ); μ].toNNReal)
Tactic: refine ⟨fun h ↦ h.charFunDual_eq, fun h ↦ ⟨fun L ↦ Measure.ext_of_charFun ?_⟩⟩
-- 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
⊢ charFun (mE := Real.measurableSpace) (Measure.map (⇑L : (a : E) → ℝ) μ) =
    charFun (gaussianReal (∫ (x : E), (L : (a : E) → ℝ) x ∂μ) Var[(⇑L : (a : E) → ℝ); μ].toNNReal)
have h₁ : ∀ (u : ℝ),
  charFun (mE := Real.measurableSpace) (Measure.map (⇑L : (a : E) → ℝ) μ) u =
    charFun (gaussianReal (∫ (x : E), (L : (a : E) → ℝ) x ∂μ) Var[(⇑L : (a : E) → ℝ); μ].toNNReal) u
Tactic: ext u
-- 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 : ℝ
⊢ charFun (mE := Real.measurableSpace) (Measure.map (⇑L : (a : E) → ℝ) μ) u =
    charFun (gaussianReal (∫ (x : E), (L : (a : E) → ℝ) x ∂μ) Var[(⇑L : (a : E) → ℝ); μ].toNNReal) u
have h₁ : cexp ((∫ (x : E), (↑((u • L : (a : E) → ℝ) x) : ℂ) ∂μ) * I - (↑Var[(⇑(u • L) : (a : E) → ℝ); μ] : ℂ) / 2) =
  cexp
    ((↑u : ℂ) * (↑(∫ (x : E), (L : (a : E) → ℝ) x ∂μ) : ℂ) * I -
      (↑(↑Var[(⇑L : (a : E) → ℝ); μ].toNNReal : ℝ) : ℂ) * HPow.hPow (β := ℕ) (↑u : ℂ) 2 / 2)
Tactic: rw [charFun_map_eq_charFunDual_smul L u, h (u • L), charFun_gaussianReal]
-- 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 : ℝ
⊢ cexp ((∫ (x : E), (↑((u • L : (a : E) → ℝ) x) : ℂ) ∂μ) * I - (↑Var[(⇑(u • L) : (a : E) → ℝ); μ] : ℂ) / 2) =
    cexp
      ((↑u : ℂ) * (↑(∫ (x : E), (L : (a : E) → ℝ) x ∂μ) : ℂ) * I -
        (↑(↑Var[(⇑L : (a : E) → ℝ); μ].toNNReal : ℝ) : ℂ) * HPow.hPow (β := ℕ) (↑u : ℂ) 2 / 2)
have h₁ : cexp
    ((∫ (x : E), (↑u : ℂ) * (↑((L : (a : E) → ℝ) x) : ℂ) ∂μ) * I -
      (↑Var[HSMul.hSMul (β := (a : E) → ℝ) u (⇑L : (a : E) → ℝ); μ] : ℂ) / 2) =
  cexp
    ((↑u : ℂ) * (↑(∫ (x : E), (L : (a : E) → ℝ) x ∂μ) : ℂ) * I -
      (↑(max Var[(⇑L : (a : E) → ℝ); μ] 0) : ℂ) * HPow.hPow (β := ℕ) (↑u : ℂ) 2 / 2)
Tactic: simp only [ContinuousLinearMap.coe_smul', Pi.smul_apply, smul_eq_mul, ofReal_mul,
    Real.coe_toNNReal']
-- 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 : ℝ
⊢ cexp
      ((∫ (x : E), (↑u : ℂ) * (↑((L : (a : E) → ℝ) x) : ℂ) ∂μ) * I -
        (↑Var[HSMul.hSMul (β := (a : E) → ℝ) u (⇑L : (a : E) → ℝ); μ] : ℂ) / 2) =
    cexp
      ((↑u : ℂ) * (↑(∫ (x : E), (L : (a : E) → ℝ) x ∂μ) : ℂ) * I -
        (↑(max Var[(⇑L : (a : E) → ℝ); μ] 0) : ℂ) * HPow.hPow (β := ℕ) (↑u : ℂ) 2 / 2)
have h₁ : ∫ (x : E), (↑u : ℂ) * (↑((L : (a : E) → ℝ) x) : ℂ) ∂μ = (↑u : ℂ) * (↑(∫ (x : E), (L : (a : E) → ℝ) x ∂μ) : ℂ)
Tactic: congr
-- 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₁ : ∫ (x : E), (↑u : ℂ) * (↑((L : (a : E) → ℝ) x) : ℂ) ∂μ = (↑u : ℂ) * (↑(∫ (x : E), (L : (a : E) → ℝ) x ∂μ) : ℂ)
⊢ cexp
      ((∫ (x : E), (↑u : ℂ) * (↑((L : (a : E) → ℝ) x) : ℂ) ∂μ) * I -
        (↑Var[HSMul.hSMul (β := (a : E) → ℝ) u (⇑L : (a : E) → ℝ); μ] : ℂ) / 2) =
    cexp
      ((↑u : ℂ) * (↑(∫ (x : E), (L : (a : E) → ℝ) x ∂μ) : ℂ) * I -
        (↑(max Var[(⇑L : (a : E) → ℝ); μ] 0) : ℂ) * HPow.hPow (β := ℕ) (↑u : ℂ) 2 / 2)
have h₂ : (↑Var[HSMul.hSMul (β := (a : E) → ℝ) u (⇑L : (a : E) → ℝ); μ] : ℂ) =
  (↑(max Var[(⇑L : (a : E) → ℝ); μ] 0) : ℂ) * HPow.hPow (β := ℕ) (↑u : ℂ) 2
Tactic: congr