awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic (goal)
Goal:
Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
X : Ω → E
inst_3 : NormedSpace ℝ E
inst_4 : IsFiniteMeasure P
hX : AEMeasurable X P
h :
  ∀ (L : StrongDual ℝ E),
    charFunDual (mE := inst_1) (Measure.map X P) L =
      cexp ((↑(∫ (x : Ω), ((⇑L : (a : E) → ℝ) ∘ X) x ∂P) : ℂ) * I - (↑Var[(⇑L : (a : E) → ℝ) ∘ X; P] : ℂ) / 2)
t : StrongDual ℝ E
hX₁ : AEMeasurable (β := ℝ) (_m := inst_1) (⇑t : (a : E) → ℝ) (Measure.map X P)
hY hφ : AEMeasurable X P
⊢ charFunDual (mE := inst_1) (Measure.map X P) t =
    cexp
      ((@integral _ _ _ _ inst_1 (Measure.map X P) fun (x : E) ↦ (↑((t : (a : E) → ℝ) x) : ℂ)) * I -
        (↑(variance (mΩ := inst_1) (⇑t : (a : E) → ℝ) (Measure.map X P)) : ℂ) / 2)
have hfm : AEStronglyMeasurable (β := ℂ) (m₀ := inst_1) (fun (x : E) ↦ (↑((t : (a : E) → ℝ) x) : ℂ)) (Measure.map X P)
Tactic: rw [h, integral_map, variance_map, integral_complex_ofReal, Function.comp_def]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic (goal)
Goal:
Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
X : Ω → E
inst_3 : NormedSpace ℝ E
L : StrongDual ℝ E
hX : HasGaussianLaw X P
⊢ charFunDual (mE := inst_1) (Measure.map X P) L =
    cexp ((↑(∫ (ω : Ω), (L : (a : E) → ℝ) (X ω) ∂P) : ℂ) * I - (↑Var[fun (ω : Ω) ↦ (L : (a : E) → ℝ) (X ω); P] : ℂ) / 2)
have rw : cexp ((↑(∫ (x : Ω), ((⇑L : (a : E) → ℝ) ∘ X) x ∂P) : ℂ) * I - (↑Var[(⇑L : (a : E) → ℝ) ∘ X; P] : ℂ) / 2) =
  cexp ((↑(∫ (ω : Ω), (L : (a : E) → ℝ) (X ω) ∂P) : ℂ) * I - (↑Var[fun (ω : Ω) ↦ (L : (a : E) → ℝ) (X ω); P] : ℂ) / 2)
Tactic: rw [hX.charFunDual_map_eq, Function.comp_def]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic (goal)
Goal:
Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
X : Ω → E
inst_3 : NormedSpace ℝ E
L : StrongDual ℝ E
hX : HasGaussianLaw X P
rw :
  cexp ((↑(∫ (x : Ω), ((⇑L : (a : E) → ℝ) ∘ X) x ∂P) : ℂ) * I - (↑Var[(⇑L : (a : E) → ℝ) ∘ X; P] : ℂ) / 2) =
    cexp ((↑(∫ (ω : Ω), (L : (a : E) → ℝ) (X ω) ∂P) : ℂ) * I - (↑Var[fun (ω : Ω) ↦ (L : (a : E) → ℝ) (X ω); P] : ℂ) / 2)
⊢ charFunDual (mE := inst_1) (Measure.map X P) L =
    cexp ((↑(∫ (ω : Ω), (L : (a : E) → ℝ) (X ω) ∂P) : ℂ) * I - (↑Var[fun (ω : Ω) ↦ (L : (a : E) → ℝ) (X ω); P] : ℂ) / 2)
have rw₁ : cexp
    ((↑(∫ (x : Ω), (fun (x : Ω) ↦ ((L : (a : E) → ℝ) (X x) : ℝ)) x ∂P) : ℂ) * I -
      (↑Var[fun (x : Ω) ↦ (L : (a : E) → ℝ) (X x); P] : ℂ) / 2) =
  cexp ((↑(∫ (ω : Ω), (L : (a : E) → ℝ) (X ω) ∂P) : ℂ) * I - (↑Var[fun (ω : Ω) ↦ (L : (a : E) → ℝ) (X ω); P] : ℂ) / 2)
Tactic: rw [hX.charFunDual_map_eq, Function.comp_def]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic (goal)
Goal:
Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
X : Ω → E
inst_3 : NormedSpace ℝ E
inst_4 : CompleteSpace E
inst_5 : SecondCountableTopology E
hX : HasGaussianLaw X P
p : ℝ≥0∞
hp : p ≠ ∞
⊢ MemLp X p P
have rw : MemLp (m0 := inst_1) id p (Measure.map X P)
Tactic: rw [← Function.id_comp X, ← memLp_map_measure_iff]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic (goal)
Goal:
Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
X : Ω → E
inst_3 : NormedSpace ℝ E
inst_4 : CompleteSpace E
inst_5 : SecondCountableTopology E
hX : HasGaussianLaw X P
p : ℝ≥0∞
hp : p ≠ ∞
rw : MemLp (m0 := inst_1) id p (Measure.map X P)
⊢ MemLp X p P
have hg : AEStronglyMeasurable (m₀ := inst_1) id (Measure.map X P)
Tactic: rw [← Function.id_comp X, ← memLp_map_measure_iff]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic (goal)
Goal:
Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
X : Ω → E
inst_3 : NormedSpace ℝ E
inst_4 : CompleteSpace E
inst_5 : SecondCountableTopology E
hX : HasGaussianLaw X P
p : ℝ≥0∞
hp : p ≠ ∞
rw : MemLp (m0 := inst_1) id p (Measure.map X P)
hg : AEStronglyMeasurable (m₀ := inst_1) id (Measure.map X P)
⊢ MemLp X p P
have hf : AEMeasurable X P
Tactic: rw [← Function.id_comp X, ← memLp_map_measure_iff]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic (goal)
Goal:
Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
X : Ω → E
inst_3 : NormedSpace ℝ E
inst_4 : CompleteSpace E
inst_5 : SecondCountableTopology E
hX : HasGaussianLaw X P
p : ℝ≥0∞
hp : p ≠ ∞
⊢ 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.Basic (goal)
Goal:
Ω : Type u_1
ι : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : Fintype ι
E : Type u_6
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : SecondCountableTopology E
X : ι → Ω → E
hX : HasGaussianLaw (E := ι → E) (fun (ω : Ω) (x : ι) ↦ X x ω) P
⊢ HasGaussianLaw.{u_1, u_6} (E := E) (∑ i : ι, X i) P
have h : Eq (α := Ω → E) (∑ i : ι, X i)
  (Function.comp (β := ι → E) (⇑(∑ i : ι, ContinuousLinearMap.proj (φ := fun (x : ι) ↦ E) i) : (a : ι → E) → E)
    fun (ω : Ω) (x : ι) ↦ X x ω)
Tactic: convert! hX.map (∑ i, .proj i)
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic (goal)
Goal:
Ω : Type u_1
ι : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : Fintype ι
E : Type u_6
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : SecondCountableTopology E
X : ι → Ω → E
hX : HasGaussianLaw (E := ι → E) (fun (ω : Ω) (x : ι) ↦ X x ω) P
⊢ Eq (α := Ω → E) (∑ i : ι, X i)
    (Function.comp (β := ι → E) (⇑(∑ i : ι, ContinuousLinearMap.proj (φ := fun (x : ι) ↦ E) i) : (a : ι → E) → E)
      fun (ω : Ω) (x : ι) ↦ X x ω)
have h : ∀ (x : Ω),
  Eq.{u_6 + 1} (α := E) ((∑ i : ι, X i) x)
    (Function.comp (β := ι → E) (⇑(∑ i : ι, ContinuousLinearMap.proj (φ := fun (x : ι) ↦ E) i) : (a : ι → E) → E)
      (fun (ω : Ω) (x : ι) ↦ X x ω) x)
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic (goal)
Goal:
Ω : Type u_1
ι : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : Fintype ι
E : Type u_6
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : SecondCountableTopology E
X : ι → Ω → E
hX : HasGaussianLaw (E := ι → E) (fun (ω : Ω) (x : ι) ↦ X x ω) P
⊢ HasGaussianLaw.{u_1, u_6} (E := E) (fun (ω : Ω) ↦ ∑ i : ι, X i ω) P
have h : ∀ (x : Ω), Eq.{u_6 + 1} (α := E) (∑ i : ι, X i x) ((∑ i : ι, X i) x)
Tactic: convert! hX.sum
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst : Fintype ι
inst_1 : DecidableEq ι
E : ι → Type u_3
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace ℝ (E i)
L_1 L : (i : ι) → StrongDual ℝ (E i) →L[ℝ] StrongDual ℝ (E i) →L[ℝ] ℝ
g : LinearMap.BilinForm ℝ (StrongDual ℝ ((i : ι) → E i)) :=
  LinearMap.mk₂ ℝ
    (fun (x y : StrongDual ℝ ((i : ι) → E i)) ↦
      ∑ i : ι,
        (((L i : (a : StrongDual ℝ (E i)) → StrongDual ℝ (E i) →L[ℝ] ℝ) (comp (σ₁₂ := RingHom.id ℝ) x (single ℝ E i)) :
              StrongDual ℝ (E i) →L[ℝ] ℝ) :
            (a : StrongDual ℝ (E i)) → ℝ)
          (comp (σ₁₂ := RingHom.id ℝ) y (single ℝ E i)))
    ⋯ ⋯ ⋯ ⋯
x y : StrongDual ℝ ((i : ι) → E i)
⊢ norm (E := ℝ)
      ((((g : (a : StrongDual ℝ ((i : ι) → E i)) → StrongDual ℝ ((i : ι) → E i) →ₗ[ℝ] ℝ) x :
              StrongDual ℝ ((i : ι) → E i) →ₗ[ℝ] ℝ) :
            (a : StrongDual ℝ ((i : ι) → E i)) → ℝ)
          y :
        ℝ) ≤
    (∑ i : ι, sorry) * ‖x‖ * ‖y‖
have simp : norm (E := ℝ)
    (∑ i : ι,
      (((L i : (a : StrongDual ℝ (E i)) → StrongDual ℝ (E i) →L[ℝ] ℝ) (comp (σ₁₂ := RingHom.id ℝ) x (single ℝ E i)) :
            StrongDual ℝ (E i) →L[ℝ] ℝ) :
          (a : StrongDual ℝ (E i)) → ℝ)
        (comp (σ₁₂ := RingHom.id ℝ) y (single ℝ E i))) ≤
  (∑ i : ι, sorry) * ‖x‖ * ‖y‖
Tactic: simp only [LinearMap.mk₂_apply, g]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst : Fintype ι
inst_1 : DecidableEq ι
E : ι → Type u_3
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace ℝ (E i)
L_1 L : (i : ι) → StrongDual ℝ (E i) →L[ℝ] StrongDual ℝ (E i) →L[ℝ] ℝ
g : LinearMap.BilinForm ℝ (StrongDual ℝ ((i : ι) → E i)) :=
  LinearMap.mk₂ ℝ
    (fun (x y : StrongDual ℝ ((i : ι) → E i)) ↦
      ∑ i : ι,
        (((L i : (a : StrongDual ℝ (E i)) → StrongDual ℝ (E i) →L[ℝ] ℝ) (comp (σ₁₂ := RingHom.id ℝ) x (single ℝ E i)) :
              StrongDual ℝ (E i) →L[ℝ] ℝ) :
            (a : StrongDual ℝ (E i)) → ℝ)
          (comp (σ₁₂ := RingHom.id ℝ) y (single ℝ E i)))
    ⋯ ⋯ ⋯ ⋯
x y : StrongDual ℝ ((i : ι) → E i)
⊢ norm (E := ℝ)
      (∑ i : ι,
        (((L i : (a : StrongDual ℝ (E i)) → StrongDual ℝ (E i) →L[ℝ] ℝ) (comp (σ₁₂ := RingHom.id ℝ) x (single ℝ E i)) :
              StrongDual ℝ (E i) →L[ℝ] ℝ) :
            (a : StrongDual ℝ (E i)) → ℝ)
          (comp (σ₁₂ := RingHom.id ℝ) y (single ℝ E i))) ≤
    (∑ i : ι, sorry) * ‖x‖ * ‖y‖
have grw : LE.le (α := ℝ)
  (∑ i : ι,
    norm (E := ℝ)
      ((((L i : (a : StrongDual ℝ (E i)) → StrongDual ℝ (E i) →L[ℝ] ℝ) (comp (σ₁₂ := RingHom.id ℝ) x (single ℝ E i)) :
              StrongDual ℝ (E i) →L[ℝ] ℝ) :
            (a : StrongDual ℝ (E i)) → ℝ)
          (comp (σ₁₂ := RingHom.id ℝ) y (single ℝ E i)) :
        ℝ))
  (∑ i : ι, sorry * ‖x‖ * ‖y‖)
Tactic: grw [norm_sum_le, sum_mul, sum_mul]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst : Fintype ι
inst_1 : DecidableEq ι
E : ι → Type u_3
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace ℝ (E i)
L_1 L : (i : ι) → StrongDual ℝ (E i) →L[ℝ] StrongDual ℝ (E i) →L[ℝ] ℝ
g : LinearMap.BilinForm ℝ (StrongDual ℝ ((i : ι) → E i)) :=
  LinearMap.mk₂ ℝ
    (fun (x y : StrongDual ℝ ((i : ι) → E i)) ↦
      ∑ i : ι,
        (((L i : (a : StrongDual ℝ (E i)) → StrongDual ℝ (E i) →L[ℝ] ℝ) (comp (σ₁₂ := RingHom.id ℝ) x (single ℝ E i)) :
              StrongDual ℝ (E i) →L[ℝ] ℝ) :
            (a : StrongDual ℝ (E i)) → ℝ)
          (comp (σ₁₂ := RingHom.id ℝ) y (single ℝ E i)))
    ⋯ ⋯ ⋯ ⋯
x y : StrongDual ℝ ((i : ι) → E i)
⊢ LE.le (α := ℝ)
    (∑ i : ι,
      norm (E := ℝ)
        ((((L i : (a : StrongDual ℝ (E i)) → StrongDual ℝ (E i) →L[ℝ] ℝ) (comp (σ₁₂ := RingHom.id ℝ) x (single ℝ E i)) :
                StrongDual ℝ (E i) →L[ℝ] ℝ) :
              (a : StrongDual ℝ (E i)) → ℝ)
            (comp (σ₁₂ := RingHom.id ℝ) y (single ℝ E i)) :
          ℝ))
    (∑ i : ι, sorry * ‖x‖ * ‖y‖)
have h : ∀ (i : ι),
  Membership.mem (γ := Finset ι) univ i →
    norm (E := ℝ)
        ((((L i : (a : StrongDual ℝ (E i)) → StrongDual ℝ (E i) →L[ℝ] ℝ) (comp (σ₁₂ := RingHom.id ℝ) x (single ℝ E i)) :
                StrongDual ℝ (E i) →L[ℝ] ℝ) :
              (a : StrongDual ℝ (E i)) → ℝ)
            (comp (σ₁₂ := RingHom.id ℝ) y (single ℝ E i)) :
          ℝ) ≤
      sorry * ‖x‖ * ‖y‖
Tactic: gcongr with i _
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst : Fintype ι
inst_1 : DecidableEq ι
E : ι → Type u_3
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace ℝ (E i)
L_1 L : (i : ι) → StrongDual ℝ (E i) →L[ℝ] StrongDual ℝ (E i) →L[ℝ] ℝ
g : LinearMap.BilinForm ℝ (StrongDual ℝ ((i : ι) → E i)) :=
  LinearMap.mk₂ ℝ
    (fun (x y : StrongDual ℝ ((i : ι) → E i)) ↦
      ∑ i : ι,
        (((L i : (a : StrongDual ℝ (E i)) → StrongDual ℝ (E i) →L[ℝ] ℝ) (comp (σ₁₂ := RingHom.id ℝ) x (single ℝ E i)) :
              StrongDual ℝ (E i) →L[ℝ] ℝ) :
            (a : StrongDual ℝ (E i)) → ℝ)
          (comp (σ₁₂ := RingHom.id ℝ) y (single ℝ E i)))
    ⋯ ⋯ ⋯ ⋯
x y : StrongDual ℝ ((i : ι) → E i)
i : ι
h : Membership.mem (γ := Finset ι) univ i
⊢ norm (E := ℝ)
      ((((L i : (a : StrongDual ℝ (E i)) → StrongDual ℝ (E i) →L[ℝ] ℝ) (comp (σ₁₂ := RingHom.id ℝ) x (single ℝ E i)) :
              StrongDual ℝ (E i) →L[ℝ] ℝ) :
            (a : StrongDual ℝ (E i)) → ℝ)
          (comp (σ₁₂ := RingHom.id ℝ) y (single ℝ E i)) :
        ℝ) ≤
    sorry * ‖x‖ * ‖y‖
have h : ‖L i‖ * (‖x‖ * 1) * (‖y‖ * 1) ≤ sorry * ‖x‖ * ‖y‖
Tactic: grw [le_opNorm₂, opNorm_comp_le, opNorm_comp_le, norm_single_le_one]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst : Fintype ι
inst_1 : DecidableEq ι
E : ι → Type u_3
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace ℝ (E i)
L_1 L : (i : ι) → StrongDual ℝ (E i) →L[ℝ] StrongDual ℝ (E i) →L[ℝ] ℝ
g : LinearMap.BilinForm ℝ (StrongDual ℝ ((i : ι) → E i)) :=
  LinearMap.mk₂ ℝ
    (fun (x y : StrongDual ℝ ((i : ι) → E i)) ↦
      ∑ i : ι,
        (((L i : (a : StrongDual ℝ (E i)) → StrongDual ℝ (E i) →L[ℝ] ℝ) (comp (σ₁₂ := RingHom.id ℝ) x (single ℝ E i)) :
              StrongDual ℝ (E i) →L[ℝ] ℝ) :
            (a : StrongDual ℝ (E i)) → ℝ)
          (comp (σ₁₂ := RingHom.id ℝ) y (single ℝ E i)))
    ⋯ ⋯ ⋯ ⋯
x y : StrongDual ℝ ((i : ι) → E i)
i : ι
h : Membership.mem (γ := Finset ι) univ i
⊢ ‖L i‖ * (‖x‖ * 1) * (‖y‖ * 1) ≤ sorry * ‖x‖ * ‖y‖
have h : ‖L i‖ * ‖x‖ * ‖y‖ ≤ sorry () * ‖x‖ * ‖y‖
Tactic: simp
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence (goal)
Goal:
ι : Type u_2
inst : Fintype ι
inst_1 : DecidableEq ι
E : ι → Type u_3
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace ℝ (E i)
L : (i : ι) → StrongDual ℝ (E i) →L[ℝ] StrongDual ℝ (E i) →L[ℝ] ℝ
hL : ∀ (i : ι), (L i).toBilinForm.IsPosSemidef
x y : StrongDual ℝ ((i : ι) → E i)
⊢ Eq (α := ℝ)
    (((((diagonalStrongDualPi (E := E) L).toBilinForm :
                (a : StrongDual ℝ ((i : ι) → E i)) → StrongDual ℝ ((i : ι) → E i) →ₗ[ℝ] ℝ)
              x :
            StrongDual ℝ ((i : ι) → E i) →ₗ[ℝ] ℝ) :
          (a : StrongDual ℝ ((i : ι) → E i)) → ℝ)
        y :
      ℝ)
    (((((diagonalStrongDualPi (E := E) L).toBilinForm :
                (a : StrongDual ℝ ((i : ι) → E i)) → StrongDual ℝ ((i : ι) → E i) →ₗ[ℝ] ℝ)
              y :
            StrongDual ℝ ((i : ι) → E i) →ₗ[ℝ] ℝ) :
          (a : StrongDual ℝ ((i : ι) → E i)) → ℝ)
        x :
      ℝ)
have simp_rw : Eq (α := ℝ)
  (∑ i : ι,
    ((((L i).toBilinForm : (a : StrongDual ℝ (E i)) → StrongDual ℝ (E i) →ₗ[ℝ] ℝ)
            (comp (σ₁₂ := RingHom.id ℝ) x (single ℝ E i)) :
          StrongDual ℝ (E i) →ₗ[ℝ] ℝ) :
        (a : StrongDual ℝ (E i)) → ℝ)
      (comp (σ₁₂ := RingHom.id ℝ) y (single ℝ E i)))
  (∑ i : ι,
    ((((L i).toBilinForm : (a : StrongDual ℝ (E i)) → StrongDual ℝ (E i) →ₗ[ℝ] ℝ)
            (comp (σ₁₂ := RingHom.id ℝ) y (single ℝ E i)) :
          StrongDual ℝ (E i) →ₗ[ℝ] ℝ) :
        (a : StrongDual ℝ (E i)) → ℝ)
      (comp (σ₁₂ := RingHom.id ℝ) x (single ℝ E i)))
Tactic: simp_rw [toBilinForm_diagonalStrongDualPi_apply, fun i ↦ (hL i).eq]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence (goal)
Goal:
ι : Type u_2
inst : Fintype ι
inst_1 : DecidableEq ι
E : ι → Type u_3
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace ℝ (E i)
L : (i : ι) → StrongDual ℝ (E i) →L[ℝ] StrongDual ℝ (E i) →L[ℝ] ℝ
hL : ∀ (i : ι), (L i).toBilinForm.IsPosSemidef
x : StrongDual ℝ ((i : ι) → E i)
⊢ LE.le (α := ℝ) (0 : ℝ)
    (((((diagonalStrongDualPi (E := E) L).toBilinForm :
                (a : StrongDual ℝ ((i : ι) → E i)) → StrongDual ℝ ((i : ι) → E i) →ₗ[ℝ] ℝ)
              x :
            StrongDual ℝ ((i : ι) → E i) →ₗ[ℝ] ℝ) :
          (a : StrongDual ℝ ((i : ι) → E i)) → ℝ)
        x :
      ℝ)
have rw : LE.le (α := ℝ) 0
  (∑ i : ι,
    ((((L i).toBilinForm : (a : StrongDual ℝ (E i)) → StrongDual ℝ (E i) →ₗ[ℝ] ℝ)
            (comp (σ₁₂ := RingHom.id ℝ) x (single ℝ E i)) :
          StrongDual ℝ (E i) →ₗ[ℝ] ℝ) :
        (a : StrongDual ℝ (E i)) → ℝ)
      (comp (σ₁₂ := RingHom.id ℝ) x (single ℝ E i)))
Tactic: rw [toBilinForm_diagonalStrongDualPi_apply]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
L₁_1 : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
L₂_1 : StrongDual ℝ F →L[ℝ] StrongDual ℝ F →L[ℝ] ℝ
L₁ : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
L₂ : StrongDual ℝ F →L[ℝ] StrongDual ℝ F →L[ℝ] ℝ
g : LinearMap.BilinForm ℝ (StrongDual ℝ (E × F)) :=
  LinearMap.mk₂ ℝ
    (fun (x y : StrongDual ℝ (E × F)) ↦
      HAdd.hAdd (α := ℝ) (β := ℝ)
        ((((L₁ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) (x ∘SL inl ℝ E F) : StrongDual ℝ E →L[ℝ] ℝ) :
              (a : StrongDual ℝ E) → ℝ)
            (y ∘SL inl ℝ E F) :
          ℝ)
        ((((L₂ : (a : StrongDual ℝ F) → StrongDual ℝ F →L[ℝ] ℝ) (x ∘SL inr ℝ E F) : StrongDual ℝ F →L[ℝ] ℝ) :
              (a : StrongDual ℝ F) → ℝ)
            (y ∘SL inr ℝ E F) :
          ℝ))
    ⋯ ⋯ ⋯ ⋯
x y : StrongDual ℝ (E × F)
⊢ norm (E := ℝ)
      ((((g : (a : StrongDual ℝ (E × F)) → StrongDual ℝ (E × F) →ₗ[ℝ] ℝ) x : StrongDual ℝ (E × F) →ₗ[ℝ] ℝ) :
            (a : StrongDual ℝ (E × F)) → ℝ)
          y :
        ℝ) ≤
    HAdd.hAdd (α := ℝ) sorry sorry * ‖x‖ * ‖y‖
have simp : ‖HAdd.hAdd (α := ℝ) (β := ℝ)
      ((((L₁ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) (x ∘SL inl ℝ E F) : StrongDual ℝ E →L[ℝ] ℝ) :
            (a : StrongDual ℝ E) → ℝ)
          (y ∘SL inl ℝ E F) :
        ℝ)
      ((((L₂ : (a : StrongDual ℝ F) → StrongDual ℝ F →L[ℝ] ℝ) (x ∘SL inr ℝ E F) : StrongDual ℝ F →L[ℝ] ℝ) :
            (a : StrongDual ℝ F) → ℝ)
          (y ∘SL inr ℝ E F) :
        ℝ)‖ ≤
  HAdd.hAdd (α := ℝ) sorry sorry * ‖x‖ * ‖y‖
Tactic: simp only [LinearMap.mk₂_apply, g]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
L₁_1 : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
L₂_1 : StrongDual ℝ F →L[ℝ] StrongDual ℝ F →L[ℝ] ℝ
L₁ : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
L₂ : StrongDual ℝ F →L[ℝ] StrongDual ℝ F →L[ℝ] ℝ
g : LinearMap.BilinForm ℝ (StrongDual ℝ (E × F)) :=
  LinearMap.mk₂ ℝ
    (fun (x y : StrongDual ℝ (E × F)) ↦
      HAdd.hAdd (α := ℝ) (β := ℝ)
        ((((L₁ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) (x ∘SL inl ℝ E F) : StrongDual ℝ E →L[ℝ] ℝ) :
              (a : StrongDual ℝ E) → ℝ)
            (y ∘SL inl ℝ E F) :
          ℝ)
        ((((L₂ : (a : StrongDual ℝ F) → StrongDual ℝ F →L[ℝ] ℝ) (x ∘SL inr ℝ E F) : StrongDual ℝ F →L[ℝ] ℝ) :
              (a : StrongDual ℝ F) → ℝ)
            (y ∘SL inr ℝ E F) :
          ℝ))
    ⋯ ⋯ ⋯ ⋯
x y : StrongDual ℝ (E × F)
⊢ ‖HAdd.hAdd (α := ℝ) (β := ℝ)
        ((((L₁ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) (x ∘SL inl ℝ E F) : StrongDual ℝ E →L[ℝ] ℝ) :
              (a : StrongDual ℝ E) → ℝ)
            (y ∘SL inl ℝ E F) :
          ℝ)
        ((((L₂ : (a : StrongDual ℝ F) → StrongDual ℝ F →L[ℝ] ℝ) (x ∘SL inr ℝ E F) : StrongDual ℝ F →L[ℝ] ℝ) :
              (a : StrongDual ℝ F) → ℝ)
            (y ∘SL inr ℝ E F) :
          ℝ)‖ ≤
    HAdd.hAdd (α := ℝ) sorry sorry * ‖x‖ * ‖y‖
have grw : norm (E := ℝ)
      ((((L₁ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) (x ∘SL inl ℝ E F) : StrongDual ℝ E →L[ℝ] ℝ) :
            (a : StrongDual ℝ E) → ℝ)
          (y ∘SL inl ℝ E F) :
        ℝ) +
    norm (E := ℝ)
      ((((L₂ : (a : StrongDual ℝ F) → StrongDual ℝ F →L[ℝ] ℝ) (x ∘SL inr ℝ E F) : StrongDual ℝ F →L[ℝ] ℝ) :
            (a : StrongDual ℝ F) → ℝ)
          (y ∘SL inr ℝ E F) :
        ℝ) ≤
  sorry * ‖x‖ * ‖y‖ + sorry * ‖x‖ * ‖y‖
Tactic: grw [norm_add_le, add_mul, add_mul]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
L₁_1 : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
L₂_1 : StrongDual ℝ F →L[ℝ] StrongDual ℝ F →L[ℝ] ℝ
L₁ : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
L₂ : StrongDual ℝ F →L[ℝ] StrongDual ℝ F →L[ℝ] ℝ
g : LinearMap.BilinForm ℝ (StrongDual ℝ (E × F)) :=
  LinearMap.mk₂ ℝ
    (fun (x y : StrongDual ℝ (E × F)) ↦
      HAdd.hAdd (α := ℝ) (β := ℝ)
        ((((L₁ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) (x ∘SL inl ℝ E F) : StrongDual ℝ E →L[ℝ] ℝ) :
              (a : StrongDual ℝ E) → ℝ)
            (y ∘SL inl ℝ E F) :
          ℝ)
        ((((L₂ : (a : StrongDual ℝ F) → StrongDual ℝ F →L[ℝ] ℝ) (x ∘SL inr ℝ E F) : StrongDual ℝ F →L[ℝ] ℝ) :
              (a : StrongDual ℝ F) → ℝ)
            (y ∘SL inr ℝ E F) :
          ℝ))
    ⋯ ⋯ ⋯ ⋯
x y : StrongDual ℝ (E × F)
⊢ norm (E := ℝ)
        ((((L₁ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) (x ∘SL inl ℝ E F) : StrongDual ℝ E →L[ℝ] ℝ) :
              (a : StrongDual ℝ E) → ℝ)
            (y ∘SL inl ℝ E F) :
          ℝ) +
      norm (E := ℝ)
        ((((L₂ : (a : StrongDual ℝ F) → StrongDual ℝ F →L[ℝ] ℝ) (x ∘SL inr ℝ E F) : StrongDual ℝ F →L[ℝ] ℝ) :
              (a : StrongDual ℝ F) → ℝ)
            (y ∘SL inr ℝ E F) :
          ℝ) ≤
    sorry * ‖x‖ * ‖y‖ + sorry * ‖x‖ * ‖y‖
have h₁ : norm (E := ℝ)
    ((((L₁ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) (x ∘SL inl ℝ E F) : StrongDual ℝ E →L[ℝ] ℝ) :
          (a : StrongDual ℝ E) → ℝ)
        (y ∘SL inl ℝ E F) :
      ℝ) ≤
  sorry * ‖x‖ * ‖y‖
Tactic: gcongr