awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
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
rw₂ 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
⊢ 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

Tactic:
rw [Measure.map_map (by fun_prop) hL, ← ContinuousLinearMap.coe_comp',
    IsGaussian.map_eq_gaussianReal]

Premises used: ContinuousLinearMap.coe_comp', ProbabilityTheory.IsGaussian.map_eq_gaussianReal, MeasureTheory.Measure.map_map
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
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 μ
x : E
L : StrongDual ℝ E
⊢ Measure.map (⇑L : (a : E) → ℝ) (Measure.dirac x) =
    gaussianReal (@integral _ _ _ _ inst_2 (Measure.dirac x) fun (x : E) ↦ (L : (a : E) → ℝ) x)
      (variance (mΩ := inst_2) (⇑L : (a : E) → ℝ) (Measure.dirac x)).toNNReal

Tactic:
simp
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
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.{u_1} (E := E) (mE := inst_2) (Measure.dirac 0)

Tactic:
instIsGaussianDirac (x := (0 : E))

Premises used: ProbabilityTheory.instIsGaussianDirac
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
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 μ
h : μ = Measure.dirac 0
⊢ IsGaussian μ

Tactic:
convert! instIsGaussianDirac (x := (0 : E))

Premises used: ProbabilityTheory.instIsGaussianDirac
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
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 μ
h :
  ∀ (s : Set E),
    Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (((Measure.dirac 0 : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
⊢ μ = Measure.dirac 0

Tactic:
ext s -
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
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∞)
h₁ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) Set.univ : ℝ≥0∞)
    (((Measure.dirac 0 : Measure E) : (a : Set E) → ℝ≥0∞) Set.univ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (((Measure.dirac 0 : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
apply Subsingleton.set_cases (p := fun s ↦ μ s = _)

Premises used: Subsingleton.set_cases
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
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∞) ∅ : ℝ≥0∞) (((Measure.dirac 0 : Measure E) : (a : Set E) → ℝ≥0∞) ∅ : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
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∞) Set.univ : ℝ≥0∞)
    (((Measure.dirac 0 : Measure E) : (a : Set E) → ℝ≥0∞) Set.univ : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
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 ≠ ∞
⊢ AEStronglyMeasurable (α := ℝ) (m₀ := Real.measurableSpace) id (Measure.map (⇑L : (a : E) → ℝ) μ)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
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 ≠ ∞
⊢ AEMeasurable (β := ℝ) (⇑L : (a : E) → ℝ) μ

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
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 ≠ ∞
rw : MemLp id p (gaussianReal (∫ (x : E), (L : (a : E) → ℝ) x ∂μ) Var[(⇑L : (a : E) → ℝ); μ].toNNReal)
⊢ MemLp (ε := ℝ) (id ∘ (⇑L : (a : E) → ℝ)) p μ

Tactic:
rw [← memLp_map_measure_iff (by fun_prop) (by fun_prop), IsGaussian.map_eq_gaussianReal L]

Premises used: ProbabilityTheory.IsGaussian.map_eq_gaussianReal, MeasureTheory.memLp_map_measure_iff
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
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.toNNReal : ℝ≥0∞) (gaussianReal (∫ (x : E), (L : (a : E) → ℝ) x ∂μ) Var[(⇑L : (a : E) → ℝ); μ].toNNReal)

Tactic:
memLp_id_gaussianReal p.toNNReal

Premises used: ENNReal.toNNReal, ProbabilityTheory.memLp_id_gaussianReal
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
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 ≠ ∞
h : p = (↑p.toNNReal : ℝ≥0∞)
⊢ MemLp id p (gaussianReal (∫ (x : E), (L : (a : E) → ℝ) x ∂μ) Var[(⇑L : (a : E) → ℝ); μ].toNNReal)

Tactic:
convert! memLp_id_gaussianReal p.toNNReal

Premises used: ENNReal.toNNReal, ProbabilityTheory.memLp_id_gaussianReal
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
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 ≠ ∞
⊢ p = (↑p.toNNReal : ℝ≥0∞)

Tactic:
simp [hp]
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
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
rw : MemLp (ε := ℝ) (⇑L : (a : E) → ℝ) 1 μ
⊢ Integrable (ε := ℝ) (⇑L : (a : E) → ℝ) μ

Tactic:
rw [← memLp_one_iff_integrable]

Premises used: MeasureTheory.memLp_one_iff_integrable
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
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
⊢ Ne (α := ℝ≥0∞) 1 ∞

Tactic:
simp
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
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
⊢ MemLp (ε := ℝ) (⇑L : (a : E) → ℝ) 1 μ

Tactic:
exact IsGaussian.memLp_dual μ L 1 (by simp)

Premises used: ProbabilityTheory.IsGaussian.memLp_dual, OfNat.ofNat
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
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 μ
L : E →L[ℝ] F
⊢ Measurable.{u_1, u_2} (α := E) (β := F) (⇑L : (a : E) → F)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
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 μ
L : E ≃L[ℝ] F
⊢ IsGaussian.{u_2} (E := F) (mE := inst_6) (Measure.map (⇑L : (a : E) → F) μ)

Tactic:
isGaussian_map (L : E →L[ℝ] F)

Premises used: ProbabilityTheory.isGaussian_map, ContinuousLinearEquiv.toContinuousLinearMap
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
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 μ

Tactic:
⟨fun h ↦ ?_, fun _ ↦ inferInstance⟩

Premises used: inferInstance, Iff.intro
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
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
refine : ∀ (h : IsGaussian.{u_2} (E := F) (mE := inst_6) (Measure.map (⇑L : (a : E) → F) μ)), IsGaussian μ
⊢ IsGaussian.{u_2} (E := F) (mE := inst_6) (Measure.map (⇑L : (a : E) → F) μ) ↔ IsGaussian μ

Tactic:
refine ⟨fun h ↦ ?_, fun _ ↦ inferInstance⟩
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
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) μ)
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) μ))
⊢ IsGaussian μ

Tactic:
rw [this]
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
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.{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:
infer_instance
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
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) μ)
suffices : μ = Measure.map.{u_2, u_1} (α := F) (⇑L.symm : (a : F) → E) (Measure.map (⇑L : (a : E) → F) μ)
⊢ IsGaussian μ

Tactic:
suffices μ = (μ.map L).map L.symm by rw [this]; infer_instance
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
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
funProp₁ : MeasurableEmbedding.{u_2, u_1} (β := E) fun (a : F) ↦ (L.symm : (a : F) → E) a
⊢ Measurable.{u_2, u_1} (α := F) (β := E) (⇑L.symm : (a : F) → E)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
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
funProp₁ : MeasurableEmbedding.{u_1, u_2} (β := F) fun (a : E) ↦ (L : (a : E) → F) a
⊢ Measurable.{u_1, u_2} (α := E) (β := F) (⇑L : (a : E) → F)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
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) μ)
rw : μ = Measure.map (Function.comp.{u_1 + 1, u_2 + 1, u_1 + 1} (β := F) (⇑L.symm : (a : F) → E) (⇑L : (a : E) → F)) μ
⊢ μ = Measure.map.{u_2, u_1} (α := F) (⇑L.symm : (a : F) → E) (Measure.map (⇑L : (a : E) → F) μ)

Tactic:
rw [Measure.map_map (by fun_prop) (by fun_prop)]

Premises used: MeasureTheory.Measure.map_map
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
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 (Function.comp.{u_1 + 1, u_2 + 1, u_1 + 1} (β := F) (⇑L.symm : (a : F) → E) (⇑L : (a : E) → F)) μ

Tactic:
simp
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
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
rw rw₁ :
  charFun (E := ℝ) (mE := Real.measurableSpace) (Measure.map (⇑L : (a : E) → ℝ) μ) 1 =
    charFun (E := ℝ) (mE := Real.measurableSpace) (Measure.map (⇑L : (a : E) → ℝ) μ) 1
⊢ charFunDual μ L = charFun (E := ℝ) (mE := Real.measurableSpace) (Measure.map (⇑L : (a : E) → ℝ) μ) 1

Tactic:
rw [charFunDual_eq_charFun_map_one]

Premises used: MeasureTheory.charFunDual_eq_charFun_map_one
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
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
rw 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
⊢ 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:
rw [IsGaussian.map_eq_gaussianReal L]

Premises used: ProbabilityTheory.IsGaussian.map_eq_gaussianReal
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
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
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)
⊢ 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:
rw [charFun_gaussianReal]

Premises used: ProbabilityTheory.charFun_gaussianReal
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
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
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)
⊢ 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:
simp only [ofReal_one, one_mul, Real.coe_toNNReal', one_pow, mul_one]

Premises used: one_pow, Real.coe_toNNReal', Complex.ofReal_one, mul_one, one_mul
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
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) : ℂ) ∂μ
e_z₁ : max Var[(⇑L : (a : E) → ℝ); μ] 0 = Var[(⇑L : (a : 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)

Tactic:
congr
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
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 e_z₁ : (↑(∫ (x : E), (L : (a : E) → ℝ) x ∂μ) : ℂ) = (↑(∫ (x : E), (L : (a : E) → ℝ) x ∂μ) : ℂ)
⊢ (↑(∫ (x : E), (L : (a : E) → ℝ) x ∂μ) : ℂ) = ∫ (x : E), (↑((L : (a : E) → ℝ) x) : ℂ) ∂μ

Tactic:
rw [integral_complex_ofReal]

Premises used: integral_complex_ofReal
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
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 : 0 ≤ Var[(⇑L : (a : E) → ℝ); μ]
⊢ max Var[(⇑L : (a : E) → ℝ); μ] 0 = Var[(⇑L : (a : E) → ℝ); μ]

Tactic:
simp only [sup_eq_left]

Premises used: sup_eq_left
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
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
⊢ 0 ≤ Var[(⇑L : (a : E) → ℝ); μ]

Tactic:
variance_nonneg _ _

Premises used: ProbabilityTheory.variance_nonneg
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
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
⊢ 0 ≤ Var[(⇑L : (a : E) → ℝ); μ]

Tactic:
exact variance_nonneg _ _

Premises used: ProbabilityTheory.variance_nonneg
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
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
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)
⊢ charFunDual μ L = 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 _ _

Premises used: HMul.hMul, HSub.hSub, ProbabilityTheory.gaussianReal, MeasureTheory.charFunDual, MeasureTheory.charFun, HDiv.hDiv, Complex.ofReal, ProbabilityTheory.variance, MeasureTheory.integral, MeasureTheory.Measure.map, Complex.exp, OfNat.ofNat, DFunLike.coe, Real.toNNReal, Complex.I
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
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)

Tactic:
⟨fun h ↦ h.charFunDual_eq, fun h ↦ ⟨fun L ↦ Measure.ext_of_charFun ?_⟩⟩

Premises used: ProbabilityTheory.IsGaussian.mk, ProbabilityTheory.IsGaussian.charFunDual_eq, MeasureTheory.Measure.ext_of_charFun, Iff.intro
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
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 μ
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)
⊢ IsGaussian μ ↔
    ∀ (L : StrongDual ℝ E),
      charFunDual μ L = cexp ((∫ (x : E), (↑((L : (a : E) → ℝ) x) : ℂ) ∂μ) * I - (↑Var[(⇑L : (a : E) → ℝ); μ] : ℂ) / 2)

Tactic:
refine ⟨fun h ↦ h.charFunDual_eq, fun h ↦ ⟨fun L ↦ Measure.ext_of_charFun ?_⟩⟩
-- Module: Mathlib.Probability.Distributions.Gaussian.Basic
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
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
⊢ charFun (mE := Real.measurableSpace) (Measure.map (⇑L : (a : E) → ℝ) μ) =
    charFun (gaussianReal (∫ (x : E), (L : (a : E) → ℝ) x ∂μ) Var[(⇑L : (a : E) → ℝ); μ].toNNReal)

Tactic:
ext u