Module: Mathlib.Probability.Distributions.Gaussian.CharFun

Goal state before:
pp: E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SecondCountableTopology E
inst✝⁴ : CompleteSpace E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : IsFiniteMeasure μ
⊢ (∃ m f, f.toBilinForm.IsPosSemidef ∧ ∀ (L : StrongDual ℝ E), charFunDual μ L = cexp (↑(L m) * I - ↑((f L) L) / 2)) ↔
    ∃ m f, f.toBilinForm.IsPosSemidef ∧ ∀ (t : E), charFun μ t = cexp (↑⟪t, m⟫ * I - ↑((f t) t) / 2)

Tactic:
refine ⟨fun ⟨m, f, hf, h⟩ ↦ ⟨m,
    f.bilinearComp (InnerProductSpace.toDualMap ℝ E).toContinuousLinearMap
      (InnerProductSpace.toDualMap ℝ E).toContinuousLinearMap,
    ⟨⟨fun x y ↦ ?_⟩, ⟨fun x ↦ ?_⟩⟩, ?_⟩,
    fun ⟨m, f, hf, h⟩ ↦ ⟨m,
      f.bilinearComp (InnerProductSpace.toDual ℝ E).symm.toLinearIsometry.toContinuousLinearMap
        (InnerProductSpace.toDual ℝ E).symm.toLinearIsometry.toContinuousLinearMap,
    ⟨⟨fun x y ↦ ?_⟩, ⟨fun x ↦ ?_⟩⟩, ?_⟩⟩

Goal state after:
case refine_1
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SecondCountableTopology E
inst✝⁴ : CompleteSpace E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : IsFiniteMeasure μ
x✝ : ∃ m f, f.toBilinForm.IsPosSemidef ∧ ∀ (L : StrongDual ℝ E), charFunDual μ L = cexp (↑(L m) * I - ↑((f L) L) / 2)
m : E
f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
hf : f.toBilinForm.IsPosSemidef
h : ∀ (L : StrongDual ℝ E), charFunDual μ L = cexp (↑(L m) * I - ↑((f L) L) / 2)
x y : E
⊢ ((f.bilinearComp (InnerProductSpace.toDualMap ℝ E).toContinuousLinearMap
            (InnerProductSpace.toDualMap ℝ E).toContinuousLinearMap).toBilinForm
        x)
      y =
    ((f.bilinearComp (InnerProductSpace.toDualMap ℝ E).toContinuousLinearMap
            (InnerProductSpace.toDualMap ℝ E).toContinuousLinearMap).toBilinForm
        y)
      x

case refine_2
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SecondCountableTopology E
inst✝⁴ : CompleteSpace E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : IsFiniteMeasure μ
x✝ : ∃ m f, f.toBilinForm.IsPosSemidef ∧ ∀ (L : StrongDual ℝ E), charFunDual μ L = cexp (↑(L m) * I - ↑((f L) L) / 2)
m : E
f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
hf : f.toBilinForm.IsPosSemidef
h : ∀ (L : StrongDual ℝ E), charFunDual μ L = cexp (↑(L m) * I - ↑((f L) L) / 2)
x : E
⊢ 0 ≤
    ((f.bilinearComp (InnerProductSpace.toDualMap ℝ E).toContinuousLinearMap
            (InnerProductSpace.toDualMap ℝ E).toContinuousLinearMap).toBilinForm
        x)
      x

case refine_3
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SecondCountableTopology E
inst✝⁴ : CompleteSpace E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : IsFiniteMeasure μ
x✝ : ∃ m f, f.toBilinForm.IsPosSemidef ∧ ∀ (L : StrongDual ℝ E), charFunDual μ L = cexp (↑(L m) * I - ↑((f L) L) / 2)
m : E
f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
hf : f.toBilinForm.IsPosSemidef
h : ∀ (L : StrongDual ℝ E), charFunDual μ L = cexp (↑(L m) * I - ↑((f L) L) / 2)
⊢ ∀ (t : E),
    charFun μ t =
      cexp
        (↑⟪t, m⟫ * I -
          ↑(((f.bilinearComp (InnerProductSpace.toDualMap ℝ E).toContinuousLinearMap
                    (InnerProductSpace.toDualMap ℝ E).toContinuousLinearMap)
                  t)
                t) /
            2)

case refine_4
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SecondCountableTopology E
inst✝⁴ : CompleteSpace E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : IsFiniteMeasure μ
x✝ : ∃ m f, f.toBilinForm.IsPosSemidef ∧ ∀ (t : E), charFun μ t = cexp (↑⟪t, m⟫ * I - ↑((f t) t) / 2)
m : E
f : E →L[ℝ] E →L[ℝ] ℝ
hf : f.toBilinForm.IsPosSemidef
h : ∀ (t : E), charFun μ t = cexp (↑⟪t, m⟫ * I - ↑((f t) t) / 2)
x y : StrongDual ℝ E
⊢ ((f.bilinearComp (InnerProductSpace.toDual ℝ E).symm.toLinearIsometry.toContinuousLinearMap
            (InnerProductSpace.toDual ℝ E).symm.toLinearIsometry.toContinuousLinearMap).toBilinForm
        x)
      y =
    ((f.bilinearComp (InnerProductSpace.toDual ℝ E).symm.toLinearIsometry.toContinuousLinearMap
            (InnerProductSpace.toDual ℝ E).symm.toLinearIsometry.toContinuousLinearMap).toBilinForm
        y)
      x

case refine_5
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SecondCountableTopology E
inst✝⁴ : CompleteSpace E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : IsFiniteMeasure μ
x✝ : ∃ m f, f.toBilinForm.IsPosSemidef ∧ ∀ (t : E), charFun μ t = cexp (↑⟪t, m⟫ * I - ↑((f t) t) / 2)
m : E
f : E →L[ℝ] E →L[ℝ] ℝ
hf : f.toBilinForm.IsPosSemidef
h : ∀ (t : E), charFun μ t = cexp (↑⟪t, m⟫ * I - ↑((f t) t) / 2)
x : StrongDual ℝ E
⊢ 0 ≤
    ((f.bilinearComp (InnerProductSpace.toDual ℝ E).symm.toLinearIsometry.toContinuousLinearMap
            (InnerProductSpace.toDual ℝ E).symm.toLinearIsometry.toContinuousLinearMap).toBilinForm
        x)
      x

case refine_6
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SecondCountableTopology E
inst✝⁴ : CompleteSpace E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : IsFiniteMeasure μ
x✝ : ∃ m f, f.toBilinForm.IsPosSemidef ∧ ∀ (t : E), charFun μ t = cexp (↑⟪t, m⟫ * I - ↑((f t) t) / 2)
m : E
f : E →L[ℝ] E →L[ℝ] ℝ
hf : f.toBilinForm.IsPosSemidef
h : ∀ (t : E), charFun μ t = cexp (↑⟪t, m⟫ * I - ↑((f t) t) / 2)
⊢ ∀ (L : StrongDual ℝ E),
    charFunDual μ L =
      cexp
        (↑(L m) * I -
          ↑(((f.bilinearComp (InnerProductSpace.toDual ℝ E).symm.toLinearIsometry.toContinuousLinearMap
                    (InnerProductSpace.toDual ℝ E).symm.toLinearIsometry.toContinuousLinearMap)
                  L)
                L) /
            2)