awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
mF : MeasurableSpace F
μ : Measure E
ν : Measure F
inst_4 : BorelSpace E
inst_5 : SecondCountableTopology E
inst_6 : BorelSpace F
inst_7 : SecondCountableTopology F
inst_8 : CompleteSpace E
inst_9 : CompleteSpace F
ξ : Measure (E × F)
inst_10 : IsFiniteMeasure μ
inst_11 : IsFiniteMeasure ν
inst_12 : IsFiniteMeasure ξ
h :
  ∀ (L : StrongDual ℝ (E × F)),
    charFunDual ξ L =
      charFunDual μ (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E F)) *
        charFunDual ν (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E F))
⊢ ξ = μ.prod ν

Tactic:
Measure.ext_of_charFunDual <| funext fun t ↦ ?_

Premises used: funext, MeasureTheory.Measure.ext_of_charFunDual
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
mF : MeasurableSpace F
μ : Measure E
ν : Measure F
inst_4 : BorelSpace E
inst_5 : SecondCountableTopology E
inst_6 : BorelSpace F
inst_7 : SecondCountableTopology F
inst_8 : CompleteSpace E
inst_9 : CompleteSpace F
ξ : Measure (E × F)
inst_10 : IsFiniteMeasure μ
inst_11 : IsFiniteMeasure ν
inst_12 : IsFiniteMeasure ξ
h :
  ∀ (L : StrongDual ℝ (E × F)),
    charFunDual ξ L =
      charFunDual μ (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E F)) *
        charFunDual ν (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E F))
refine : ∀ (t : StrongDual ℝ (E × F)), charFunDual ξ t = charFunDual (μ.prod ν) t
⊢ ξ = μ.prod ν

Tactic:
refine Measure.ext_of_charFunDual <| funext fun t ↦ ?_

Premises used: funext, MeasureTheory.Measure.ext_of_charFunDual
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
mF : MeasurableSpace F
μ : Measure E
ν : Measure F
inst_4 : BorelSpace E
inst_5 : SecondCountableTopology E
inst_6 : BorelSpace F
inst_7 : SecondCountableTopology F
inst_8 : CompleteSpace E
inst_9 : CompleteSpace F
ξ : Measure (E × F)
inst_10 : IsFiniteMeasure μ
inst_11 : IsFiniteMeasure ν
inst_12 : IsFiniteMeasure ξ
h :
  ∀ (L : StrongDual ℝ (E × F)),
    charFunDual ξ L =
      charFunDual μ (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E F)) *
        charFunDual ν (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E F))
t : StrongDual ℝ (E × F)
rw :
  charFunDual μ (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) t (ContinuousLinearMap.inl ℝ E F)) *
      charFunDual ν (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) t (ContinuousLinearMap.inr ℝ E F)) =
    charFunDual (μ.prod ν) t
rw₁ rw₂ :
  charFunDual μ (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) t (ContinuousLinearMap.inl ℝ E F)) *
      charFunDual ν (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) t (ContinuousLinearMap.inr ℝ E F)) =
    charFunDual μ (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) t (ContinuousLinearMap.inl ℝ E F)) *
      charFunDual ν (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) t (ContinuousLinearMap.inr ℝ E F))
⊢ charFunDual ξ t = charFunDual (μ.prod ν) t

Tactic:
rw [h, charFunDual_prod]

Premises used: MeasureTheory.charFunDual_prod
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
mF : MeasurableSpace F
μ : Measure E
ν : Measure F
inst_4 : BorelSpace E
inst_5 : SecondCountableTopology E
inst_6 : BorelSpace F
inst_7 : SecondCountableTopology F
inst_8 : CompleteSpace E
inst_9 : CompleteSpace F
ξ : Measure (E × F)
inst_10 : IsFiniteMeasure μ
inst_11 : IsFiniteMeasure ν
inst_12 : IsFiniteMeasure ξ
h : ξ = μ.prod ν
rw :
  ∀ (L : StrongDual ℝ (E × F)),
    charFunDual (μ.prod ν) L =
      charFunDual μ (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E F)) *
        charFunDual ν (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E F))
⊢ ∀ (L : StrongDual ℝ (E × F)),
    charFunDual ξ L =
      charFunDual μ (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E F)) *
        charFunDual ν (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E F))

Tactic:
rw [h]
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
mF : MeasurableSpace F
μ : Measure E
ν : Measure F
inst_4 : BorelSpace E
inst_5 : SecondCountableTopology E
inst_6 : BorelSpace F
inst_7 : SecondCountableTopology F
inst_8 : CompleteSpace E
inst_9 : CompleteSpace F
ξ : Measure (E × F)
inst_10 : IsFiniteMeasure μ
inst_11 : IsFiniteMeasure ν
inst_12 : IsFiniteMeasure ξ
h : ξ = μ.prod ν
⊢ ∀ (L : StrongDual ℝ (E × F)),
    charFunDual (μ.prod ν) L =
      charFunDual μ (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E F)) *
        charFunDual ν (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E F))

Tactic:
charFunDual_prod

Premises used: MeasureTheory.charFunDual_prod, setOf
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
mF : MeasurableSpace F
μ : Measure E
ν : Measure F
inst_4 : BorelSpace E
inst_5 : SecondCountableTopology E
inst_6 : BorelSpace F
inst_7 : SecondCountableTopology F
inst_8 : CompleteSpace E
inst_9 : CompleteSpace F
ξ : Measure (E × F)
inst_10 : IsFiniteMeasure μ
inst_11 : IsFiniteMeasure ν
inst_12 : IsFiniteMeasure ξ
h : ξ = μ.prod ν
⊢ ∀ (L : StrongDual ℝ (E × F)),
    charFunDual (μ.prod ν) L =
      charFunDual μ (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E F)) *
        charFunDual ν (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E F))

Tactic:
exact charFunDual_prod

Premises used: MeasureTheory.charFunDual_prod
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
mF : MeasurableSpace F
μ : Measure E
ν : Measure F
inst_4 : BorelSpace E
inst_5 : SecondCountableTopology E
p : ℝ≥0∞
inst_6 : Fact (1 ≤ p)
inst_7 : BorelSpace F
inst_8 : SecondCountableTopology F
inst_9 : CompleteSpace E
inst_10 : CompleteSpace F
ξ : Measure (E × F)
inst_11 : IsFiniteMeasure μ
inst_12 : IsFiniteMeasure ν
inst_13 : IsFiniteMeasure ξ
h :
  ∀ (L : StrongDual ℝ (WithLp p (E × F))),
    charFunDual (mE := WithLp.measurableSpace p (E × F)) (Measure.map (toLp p) ξ) L =
      charFunDual μ
          (L ∘SL
            (↑(ContinuousLinearEquiv.symm (prodContinuousLinearEquiv p ℝ E F)) : E × F →L[ℝ] WithLp p (E × F)) ∘SL
              ContinuousLinearMap.inl ℝ E F) *
        charFunDual ν
          (L ∘SL
            (↑(ContinuousLinearEquiv.symm (prodContinuousLinearEquiv p ℝ E F)) : E × F →L[ℝ] WithLp p (E × F)) ∘SL
              ContinuousLinearMap.inr ℝ E F)
⊢ ξ = μ.prod ν

Tactic:
(MeasurableEquiv.toLp p (E × F)).map_measurableEquiv_injective
      <| Measure.ext_of_charFunDual <| funext fun L ↦ ?_

Premises used: MeasurableEquiv.toLp, funext, MeasureTheory.Measure.ext_of_charFunDual, MeasurableEquiv.map_measurableEquiv_injective, Prod
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
mF : MeasurableSpace F
μ : Measure E
ν : Measure F
inst_4 : BorelSpace E
inst_5 : SecondCountableTopology E
p : ℝ≥0∞
inst_6 : Fact (1 ≤ p)
inst_7 : BorelSpace F
inst_8 : SecondCountableTopology F
inst_9 : CompleteSpace E
inst_10 : CompleteSpace F
ξ : Measure (E × F)
inst_11 : IsFiniteMeasure μ
inst_12 : IsFiniteMeasure ν
inst_13 : IsFiniteMeasure ξ
h :
  ∀ (L : StrongDual ℝ (WithLp p (E × F))),
    charFunDual (mE := WithLp.measurableSpace p (E × F)) (Measure.map (toLp p) ξ) L =
      charFunDual μ
          (L ∘SL
            (↑(ContinuousLinearEquiv.symm (prodContinuousLinearEquiv p ℝ E F)) : E × F →L[ℝ] WithLp p (E × F)) ∘SL
              ContinuousLinearMap.inl ℝ E F) *
        charFunDual ν
          (L ∘SL
            (↑(ContinuousLinearEquiv.symm (prodContinuousLinearEquiv p ℝ E F)) : E × F →L[ℝ] WithLp p (E × F)) ∘SL
              ContinuousLinearMap.inr ℝ E F)
refine :
  ∀ (L : StrongDual ℝ (WithLp p (E × F))),
    charFunDual (mE := WithLp.measurableSpace p (E × F))
        (Measure.map (⇑(MeasurableEquiv.toLp p (E × F)) : (a : E × F) → WithLp p (E × F)) ξ) L =
      charFunDual (mE := WithLp.measurableSpace p (E × F))
        (Measure.map (⇑(MeasurableEquiv.toLp p (E × F)) : (a : E × F) → WithLp p (E × F)) (μ.prod ν)) L
⊢ ξ = μ.prod ν

Tactic:
refine (MeasurableEquiv.toLp p (E × F)).map_measurableEquiv_injective
      <| Measure.ext_of_charFunDual <| funext fun L ↦ ?_

Premises used: MeasurableEquiv.toLp, funext, MeasureTheory.Measure.ext_of_charFunDual, MeasurableEquiv.map_measurableEquiv_injective, Prod
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
mF : MeasurableSpace F
μ : Measure E
ν : Measure F
inst_4 : BorelSpace E
inst_5 : SecondCountableTopology E
p : ℝ≥0∞
inst_6 : Fact (1 ≤ p)
inst_7 : BorelSpace F
inst_8 : SecondCountableTopology F
inst_9 : CompleteSpace E
inst_10 : CompleteSpace F
ξ : Measure (E × F)
inst_11 : IsFiniteMeasure μ
inst_12 : IsFiniteMeasure ν
inst_13 : IsFiniteMeasure ξ
h :
  ∀ (L : StrongDual ℝ (WithLp p (E × F))),
    charFunDual (mE := WithLp.measurableSpace p (E × F)) (Measure.map (toLp p) ξ) L =
      charFunDual μ
          (L ∘SL
            (↑(ContinuousLinearEquiv.symm (prodContinuousLinearEquiv p ℝ E F)) : E × F →L[ℝ] WithLp p (E × F)) ∘SL
              ContinuousLinearMap.inl ℝ E F) *
        charFunDual ν
          (L ∘SL
            (↑(ContinuousLinearEquiv.symm (prodContinuousLinearEquiv p ℝ E F)) : E × F →L[ℝ] WithLp p (E × F)) ∘SL
              ContinuousLinearMap.inr ℝ E F)
L : StrongDual ℝ (WithLp p (E × F))
rw :
  charFunDual (mE := WithLp.measurableSpace p (E × F)) (Measure.map (toLp p) ξ) L =
    charFunDual (mE := WithLp.measurableSpace p (E × F)) (Measure.map (toLp p) (μ.prod ν)) L
rw₁ :
  charFunDual μ
        (L ∘SL
          (↑(ContinuousLinearEquiv.symm (prodContinuousLinearEquiv p ℝ E F)) : E × F →L[ℝ] WithLp p (E × F)) ∘SL
            ContinuousLinearMap.inl ℝ E F) *
      charFunDual ν
        (L ∘SL
          (↑(ContinuousLinearEquiv.symm (prodContinuousLinearEquiv p ℝ E F)) : E × F →L[ℝ] WithLp p (E × F)) ∘SL
            ContinuousLinearMap.inr ℝ E F) =
    charFunDual (mE := WithLp.measurableSpace p (E × F)) (Measure.map (toLp p) (μ.prod ν)) L
rw₂ rw₃ :
  charFunDual μ
        (L ∘SL
          (↑(ContinuousLinearEquiv.symm (prodContinuousLinearEquiv p ℝ E F)) : E × F →L[ℝ] WithLp p (E × F)) ∘SL
            ContinuousLinearMap.inl ℝ E F) *
      charFunDual ν
        (L ∘SL
          (↑(ContinuousLinearEquiv.symm (prodContinuousLinearEquiv p ℝ E F)) : E × F →L[ℝ] WithLp p (E × F)) ∘SL
            ContinuousLinearMap.inr ℝ E F) =
    charFunDual μ
        (L ∘SL
          (↑(ContinuousLinearEquiv.symm (prodContinuousLinearEquiv p ℝ E F)) : E × F →L[ℝ] WithLp p (E × F)) ∘SL
            ContinuousLinearMap.inl ℝ E F) *
      charFunDual ν
        (L ∘SL
          (↑(ContinuousLinearEquiv.symm (prodContinuousLinearEquiv p ℝ E F)) : E × F →L[ℝ] WithLp p (E × F)) ∘SL
            ContinuousLinearMap.inr ℝ E F)
⊢ charFunDual (mE := WithLp.measurableSpace p (E × F))
      (Measure.map (⇑(MeasurableEquiv.toLp p (E × F)) : (a : E × F) → WithLp p (E × F)) ξ) L =
    charFunDual (mE := WithLp.measurableSpace p (E × F))
      (Measure.map (⇑(MeasurableEquiv.toLp p (E × F)) : (a : E × F) → WithLp p (E × F)) (μ.prod ν)) L

Tactic:
rw [MeasurableEquiv.coe_toLp, h, charFunDual_prod']

Premises used: MeasurableEquiv.coe_toLp, MeasureTheory.charFunDual_prod'
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
mF : MeasurableSpace F
μ : Measure E
ν : Measure F
inst_4 : BorelSpace E
inst_5 : SecondCountableTopology E
p : ℝ≥0∞
inst_6 : Fact (1 ≤ p)
inst_7 : BorelSpace F
inst_8 : SecondCountableTopology F
inst_9 : CompleteSpace E
inst_10 : CompleteSpace F
ξ : Measure (E × F)
inst_11 : IsFiniteMeasure μ
inst_12 : IsFiniteMeasure ν
inst_13 : IsFiniteMeasure ξ
h : ξ = μ.prod ν
rw :
  ∀ (L : StrongDual ℝ (WithLp p (E × F))),
    charFunDual (mE := WithLp.measurableSpace p (E × F)) (Measure.map (toLp p) (μ.prod ν)) L =
      charFunDual μ
          (L ∘SL
            (↑(ContinuousLinearEquiv.symm (prodContinuousLinearEquiv p ℝ E F)) : E × F →L[ℝ] WithLp p (E × F)) ∘SL
              ContinuousLinearMap.inl ℝ E F) *
        charFunDual ν
          (L ∘SL
            (↑(ContinuousLinearEquiv.symm (prodContinuousLinearEquiv p ℝ E F)) : E × F →L[ℝ] WithLp p (E × F)) ∘SL
              ContinuousLinearMap.inr ℝ E F)
⊢ ∀ (L : StrongDual ℝ (WithLp p (E × F))),
    charFunDual (mE := WithLp.measurableSpace p (E × F)) (Measure.map (toLp p) ξ) L =
      charFunDual μ
          (L ∘SL
            (↑(ContinuousLinearEquiv.symm (prodContinuousLinearEquiv p ℝ E F)) : E × F →L[ℝ] WithLp p (E × F)) ∘SL
              ContinuousLinearMap.inl ℝ E F) *
        charFunDual ν
          (L ∘SL
            (↑(ContinuousLinearEquiv.symm (prodContinuousLinearEquiv p ℝ E F)) : E × F →L[ℝ] WithLp p (E × F)) ∘SL
              ContinuousLinearMap.inr ℝ E F)

Tactic:
rw [h]
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
mF : MeasurableSpace F
μ : Measure E
ν : Measure F
inst_4 : BorelSpace E
inst_5 : SecondCountableTopology E
p : ℝ≥0∞
inst_6 : Fact (1 ≤ p)
inst_7 : BorelSpace F
inst_8 : SecondCountableTopology F
inst_9 : CompleteSpace E
inst_10 : CompleteSpace F
ξ : Measure (E × F)
inst_11 : IsFiniteMeasure μ
inst_12 : IsFiniteMeasure ν
inst_13 : IsFiniteMeasure ξ
h : ξ = μ.prod ν
⊢ ∀ (L : StrongDual ℝ (WithLp p (E × F))),
    charFunDual (mE := WithLp.measurableSpace p (E × F)) (Measure.map (toLp p) (μ.prod ν)) L =
      charFunDual μ
          (L ∘SL
            (↑(ContinuousLinearEquiv.symm (prodContinuousLinearEquiv p ℝ E F)) : E × F →L[ℝ] WithLp p (E × F)) ∘SL
              ContinuousLinearMap.inl ℝ E F) *
        charFunDual ν
          (L ∘SL
            (↑(ContinuousLinearEquiv.symm (prodContinuousLinearEquiv p ℝ E F)) : E × F →L[ℝ] WithLp p (E × F)) ∘SL
              ContinuousLinearMap.inr ℝ E F)

Tactic:
charFunDual_prod' p

Premises used: setOf, MeasureTheory.charFunDual_prod'
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
mF : MeasurableSpace F
μ : Measure E
ν : Measure F
inst_4 : BorelSpace E
inst_5 : SecondCountableTopology E
p : ℝ≥0∞
inst_6 : Fact (1 ≤ p)
inst_7 : BorelSpace F
inst_8 : SecondCountableTopology F
inst_9 : CompleteSpace E
inst_10 : CompleteSpace F
ξ : Measure (E × F)
inst_11 : IsFiniteMeasure μ
inst_12 : IsFiniteMeasure ν
inst_13 : IsFiniteMeasure ξ
h : ξ = μ.prod ν
⊢ ∀ (L : StrongDual ℝ (WithLp p (E × F))),
    charFunDual (mE := WithLp.measurableSpace p (E × F)) (Measure.map (toLp p) (μ.prod ν)) L =
      charFunDual μ
          (L ∘SL
            (↑(ContinuousLinearEquiv.symm (prodContinuousLinearEquiv p ℝ E F)) : E × F →L[ℝ] WithLp p (E × F)) ∘SL
              ContinuousLinearMap.inl ℝ E F) *
        charFunDual ν
          (L ∘SL
            (↑(ContinuousLinearEquiv.symm (prodContinuousLinearEquiv p ℝ E F)) : E × F →L[ℝ] WithLp p (E × F)) ∘SL
              ContinuousLinearMap.inr ℝ E F)

Tactic:
exact charFunDual_prod' p

Premises used: MeasureTheory.charFunDual_prod'
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
ι : Type u_4
inst : Fintype ι
inst_1 : DecidableEq ι
E : ι → Type u_5
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace ℝ (E i)
mE : (i : ι) → MeasurableSpace (E i)
inst_4 : ∀ (i : ι), BorelSpace.{u_5} (E i)
inst_5 : ∀ (i : ι), SecondCountableTopology.{u_5} (E i)
inst_6 : ∀ (i : ι), CompleteSpace.{u_5} (E i)
μ : (i : ι) → Measure (E i)
ν : Measure ((i : ι) → E i)
inst_7 : ∀ (i : ι), IsFiniteMeasure (μ i)
inst_8 : IsFiniteMeasure ν
h :
  ∀ (L : StrongDual ℝ ((i : ι) → E i)),
    charFunDual ν L =
      ∏ i : ι, charFunDual (μ i) (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.single ℝ E i))
⊢ ν = Measure.pi (α := E) μ

Tactic:
Measure.ext_of_charFunDual <| funext fun t ↦ ?_

Premises used: funext, MeasureTheory.Measure.ext_of_charFunDual
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
ι : Type u_4
inst : Fintype ι
inst_1 : DecidableEq ι
E : ι → Type u_5
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace ℝ (E i)
mE : (i : ι) → MeasurableSpace (E i)
inst_4 : ∀ (i : ι), BorelSpace.{u_5} (E i)
inst_5 : ∀ (i : ι), SecondCountableTopology.{u_5} (E i)
inst_6 : ∀ (i : ι), CompleteSpace.{u_5} (E i)
μ : (i : ι) → Measure (E i)
ν : Measure ((i : ι) → E i)
inst_7 : ∀ (i : ι), IsFiniteMeasure (μ i)
inst_8 : IsFiniteMeasure ν
h :
  ∀ (L : StrongDual ℝ ((i : ι) → E i)),
    charFunDual ν L =
      ∏ i : ι, charFunDual (μ i) (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.single ℝ E i))
refine : ∀ (t : StrongDual ℝ ((i : ι) → E i)), charFunDual ν t = charFunDual (Measure.pi (α := E) μ) t
⊢ ν = Measure.pi (α := E) μ

Tactic:
refine Measure.ext_of_charFunDual <| funext fun t ↦ ?_

Premises used: funext, MeasureTheory.Measure.ext_of_charFunDual
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
ι : Type u_4
inst : Fintype ι
inst_1 : DecidableEq ι
E : ι → Type u_5
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace ℝ (E i)
mE : (i : ι) → MeasurableSpace (E i)
inst_4 : ∀ (i : ι), BorelSpace.{u_5} (E i)
inst_5 : ∀ (i : ι), SecondCountableTopology.{u_5} (E i)
inst_6 : ∀ (i : ι), CompleteSpace.{u_5} (E i)
μ : (i : ι) → Measure (E i)
ν : Measure ((i : ι) → E i)
inst_7 : ∀ (i : ι), IsFiniteMeasure (μ i)
inst_8 : IsFiniteMeasure ν
h :
  ∀ (L : StrongDual ℝ ((i : ι) → E i)),
    charFunDual ν L =
      ∏ i : ι, charFunDual (μ i) (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.single ℝ E i))
t : StrongDual ℝ ((i : ι) → E i)
rw :
  ∏ i : ι, charFunDual (μ i) (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) t (ContinuousLinearMap.single ℝ E i)) =
    charFunDual (Measure.pi (α := E) μ) t
rw₁ rw₂ :
  Eq (α := ℂ)
    (∏ i : ι, charFunDual (μ i) (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) t (ContinuousLinearMap.single ℝ E i)))
    (∏ i : ι, charFunDual (μ i) (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) t (ContinuousLinearMap.single ℝ E i)))
⊢ charFunDual ν t = charFunDual (Measure.pi (α := E) μ) t

Tactic:
rw [h, charFunDual_pi]

Premises used: MeasureTheory.charFunDual_pi
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
ι : Type u_4
inst : Fintype ι
inst_1 : DecidableEq ι
E : ι → Type u_5
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace ℝ (E i)
mE : (i : ι) → MeasurableSpace (E i)
inst_4 : ∀ (i : ι), BorelSpace.{u_5} (E i)
inst_5 : ∀ (i : ι), SecondCountableTopology.{u_5} (E i)
inst_6 : ∀ (i : ι), CompleteSpace.{u_5} (E i)
μ : (i : ι) → Measure (E i)
ν : Measure ((i : ι) → E i)
inst_7 : ∀ (i : ι), IsFiniteMeasure (μ i)
inst_8 : IsFiniteMeasure ν
h : ν = Measure.pi (α := E) μ
rw :
  ∀ (L : StrongDual ℝ ((i : ι) → E i)),
    charFunDual (Measure.pi (α := E) μ) L =
      ∏ i : ι, charFunDual (μ i) (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.single ℝ E i))
⊢ ∀ (L : StrongDual ℝ ((i : ι) → E i)),
    charFunDual ν L =
      ∏ i : ι, charFunDual (μ i) (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.single ℝ E i))

Tactic:
rw [h]
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
ι : Type u_4
inst : Fintype ι
inst_1 : DecidableEq ι
E : ι → Type u_5
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace ℝ (E i)
mE : (i : ι) → MeasurableSpace (E i)
inst_4 : ∀ (i : ι), BorelSpace.{u_5} (E i)
inst_5 : ∀ (i : ι), SecondCountableTopology.{u_5} (E i)
inst_6 : ∀ (i : ι), CompleteSpace.{u_5} (E i)
μ : (i : ι) → Measure (E i)
ν : Measure ((i : ι) → E i)
inst_7 : ∀ (i : ι), IsFiniteMeasure (μ i)
inst_8 : IsFiniteMeasure ν
h : ν = Measure.pi (α := E) μ
⊢ ∀ (L : StrongDual ℝ ((i : ι) → E i)),
    charFunDual (Measure.pi (α := E) μ) L =
      ∏ i : ι, charFunDual (μ i) (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.single ℝ E i))

Tactic:
charFunDual_pi

Premises used: MeasureTheory.charFunDual_pi
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
ι : Type u_4
inst : Fintype ι
inst_1 : DecidableEq ι
E : ι → Type u_5
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace ℝ (E i)
mE : (i : ι) → MeasurableSpace (E i)
inst_4 : ∀ (i : ι), BorelSpace.{u_5} (E i)
inst_5 : ∀ (i : ι), SecondCountableTopology.{u_5} (E i)
inst_6 : ∀ (i : ι), CompleteSpace.{u_5} (E i)
μ : (i : ι) → Measure (E i)
ν : Measure ((i : ι) → E i)
inst_7 : ∀ (i : ι), IsFiniteMeasure (μ i)
inst_8 : IsFiniteMeasure ν
h : ν = Measure.pi (α := E) μ
⊢ ∀ (L : StrongDual ℝ ((i : ι) → E i)),
    charFunDual (Measure.pi (α := E) μ) L =
      ∏ i : ι, charFunDual (μ i) (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.single ℝ E i))

Tactic:
exact charFunDual_pi

Premises used: MeasureTheory.charFunDual_pi
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
p : ℝ≥0∞
inst : Fact (1 ≤ p)
ι : Type u_4
inst_1 : Fintype ι
inst_2 : DecidableEq ι
E : ι → Type u_5
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace ℝ (E i)
mE : (i : ι) → MeasurableSpace (E i)
inst_5 : ∀ (i : ι), BorelSpace.{u_5} (E i)
inst_6 : ∀ (i : ι), SecondCountableTopology.{u_5} (E i)
inst_7 : ∀ (i : ι), CompleteSpace.{u_5} (E i)
μ : (i : ι) → Measure (E i)
ν : Measure ((i : ι) → E i)
inst_8 : ∀ (i : ι), IsFiniteMeasure (μ i)
inst_9 : IsFiniteMeasure ν
h :
  ∀ (L : StrongDual ℝ (WithLp p ((i : ι) → E i))),
    charFunDual (mE := WithLp.measurableSpace p ((i : ι) → E i)) (Measure.map (toLp p) ν) L =
      ∏ i : ι,
        charFunDual (μ i)
          (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L
            (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ)
              (↑(ContinuousLinearEquiv.symm (PiLp.continuousLinearEquiv p ℝ E)) : ((i : ι) → E i) →L[ℝ] PiLp p E)
              (ContinuousLinearMap.single ℝ E i)))
⊢ ν = Measure.pi (α := E) μ

Tactic:
(MeasurableEquiv.toLp p (Π i, E i)).map_measurableEquiv_injective
      <| Measure.ext_of_charFunDual <| funext fun L ↦ ?_

Premises used: MeasurableEquiv.toLp, funext, MeasureTheory.Measure.ext_of_charFunDual, MeasurableEquiv.map_measurableEquiv_injective