awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Fourier.Inversion
Goal:
V : Type u_1
E : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MeasurableSpace V
inst_3 : BorelSpace V
inst_4 : FiniteDimensional ℝ V
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℂ E
f : V → E
inst_7 : CompleteSpace E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
v : V
h'f : ContinuousAt f v
φ : V → ℝ :=
  fun (w : V) ↦
    π ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 * rexp (-HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2)
A :
  Tendsto
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦ (c ^ finrank ℝ V * φ (c • (v - w))) • f w)
    atTop (𝓝 (f v))
B :
  Tendsto
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
        ((c ^ (1 / 2)) ^ finrank ℝ V * φ (c ^ (1 / 2) • (v - w))) • f w)
    atTop (𝓝 (f v))
c : ℝ
hc : 0 < c
w : V
h :
  -HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖c ^ HDiv.hDiv (α := ℝ) 1 2 • (v - w)‖ 2 =
    -HPow.hPow (β := ℕ) π 2 * c * HPow.hPow (β := ℕ) ‖v - w‖ 2
⊢ (↑(-HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖c ^ (1 / 2) • (v - w)‖ 2) : ℂ) =
    -HPow.hPow (β := ℕ) (↑π : ℂ) 2 * (↑c : ℂ) * HPow.hPow (β := ℕ) (↑‖v - w‖ : ℂ) 2

Tactic:
norm_cast
-- Module: Mathlib.Analysis.Fourier.Inversion
Goal:
V : Type u_1
E : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MeasurableSpace V
inst_3 : BorelSpace V
inst_4 : FiniteDimensional ℝ V
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℂ E
f : V → E
inst_7 : CompleteSpace E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
v : V
h'f : ContinuousAt f v
φ : V → ℝ :=
  fun (w : V) ↦
    π ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 * rexp (-HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2)
A :
  Tendsto
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦ (c ^ finrank ℝ V * φ (c • (v - w))) • f w)
    atTop (𝓝 (f v))
B :
  Tendsto
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
        ((c ^ (1 / 2)) ^ finrank ℝ V * φ (c ^ (1 / 2) • (v - w))) • f w)
    atTop (𝓝 (f v))
c : ℝ
hc : 0 < c
w : V
h :
  HPow.hPow (β := ℝ) π (↑2 : ℝ) * (c ^ HMul.hMul (α := ℝ) 2⁻¹ (↑2 : ℝ) * HPow.hPow (β := ℝ) ‖v - w‖ (↑2 : ℝ)) =
    HPow.hPow (β := ℝ) π (↑2 : ℝ) * (c * HPow.hPow (β := ℝ) ‖v - w‖ (↑2 : ℝ))
⊢ -HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖c ^ HDiv.hDiv (α := ℝ) 1 2 • (v - w)‖ 2 =
    -HPow.hPow (β := ℕ) π 2 * c * HPow.hPow (β := ℕ) ‖v - w‖ 2

Tactic:
simp only [one_div, norm_smul, Real.norm_eq_abs, mul_pow, sq_abs, neg_mul, neg_inj,
      ← rpow_natCast, ← rpow_mul hc.le, mul_assoc]

Premises used: norm_smul, mul_assoc, LT.lt.le, one_div, neg_inj, neg_mul, sq_abs, Real.rpow_mul, mul_pow, Real.rpow_natCast, Real.norm_eq_abs
-- Module: Mathlib.Analysis.Fourier.Inversion
Goal:
V : Type u_1
E : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MeasurableSpace V
inst_3 : BorelSpace V
inst_4 : FiniteDimensional ℝ V
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℂ E
f : V → E
inst_7 : CompleteSpace E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
v : V
h'f : ContinuousAt f v
φ : V → ℝ :=
  fun (w : V) ↦
    π ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 * rexp (-HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2)
A :
  Tendsto
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦ (c ^ finrank ℝ V * φ (c • (v - w))) • f w)
    atTop (𝓝 (f v))
B :
  Tendsto
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
        ((c ^ (1 / 2)) ^ finrank ℝ V * φ (c ^ (1 / 2) • (v - w))) • f w)
    atTop (𝓝 (f v))
c : ℝ
hc : 0 < c
w : V
⊢ HPow.hPow (β := ℝ) π (↑2 : ℝ) * (c ^ HMul.hMul (α := ℝ) 2⁻¹ (↑2 : ℝ) * HPow.hPow (β := ℝ) ‖v - w‖ (↑2 : ℝ)) =
    HPow.hPow (β := ℝ) π (↑2 : ℝ) * (c * HPow.hPow (β := ℝ) ‖v - w‖ (↑2 : ℝ))

Tactic:
simp
-- Module: Mathlib.Analysis.Fourier.Inversion
Goal:
V : Type u_1
E : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MeasurableSpace V
inst_3 : BorelSpace V
inst_4 : FiniteDimensional ℝ V
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℂ E
f : V → E
inst_7 : CompleteSpace E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
h'f : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (𝓕 f) volume
v : V
hv : ContinuousAt f v
⊢ 𝓕⁻ (𝓕 f) v = f v

Tactic:
tendsto_nhds_unique (Real.tendsto_integral_gaussian_smul hf h'f v)
    (Real.tendsto_integral_gaussian_smul' hf hv)

Premises used: Real.tendsto_integral_gaussian_smul', Real.tendsto_integral_gaussian_smul, tendsto_nhds_unique
-- Module: Mathlib.Analysis.Fourier.Inversion
Goal:
V : Type u_1
E : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MeasurableSpace V
inst_3 : BorelSpace V
inst_4 : FiniteDimensional ℝ V
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℂ E
f : V → E
inst_7 : CompleteSpace E
h :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
h'f : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (𝓕 f) volume
h₁ : ∀ (v : V), 𝓕⁻ (𝓕 f) v = f v
⊢ 𝓕⁻ (𝓕 f) = f

Tactic:
ext v
-- Module: Mathlib.Analysis.Fourier.Inversion
Goal:
V : Type u_1
E : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MeasurableSpace V
inst_3 : BorelSpace V
inst_4 : FiniteDimensional ℝ V
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℂ E
f : V → E
inst_7 : CompleteSpace E
h :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
h'f : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (𝓕 f) volume
v : V
⊢ 𝓕⁻ (𝓕 f) v = f v

Tactic:
hf.fourierInv_fourier_eq h'f h.continuousAt

Premises used: MeasureTheory.Integrable.fourierInv_fourier_eq, Continuous.continuousAt
-- Module: Mathlib.Analysis.Fourier.Inversion
Goal:
V : Type u_1
E : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MeasurableSpace V
inst_3 : BorelSpace V
inst_4 : FiniteDimensional ℝ V
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℂ E
f : V → E
inst_7 : CompleteSpace E
h :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
h'f : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (𝓕 f) volume
v : V
⊢ 𝓕⁻ (𝓕 f) v = f v

Tactic:
exact hf.fourierInv_fourier_eq h'f h.continuousAt

Premises used: MeasureTheory.Integrable.fourierInv_fourier_eq, Continuous.continuousAt
-- Module: Mathlib.Analysis.Fourier.Inversion
Goal:
V : Type u_1
E : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MeasurableSpace V
inst_3 : BorelSpace V
inst_4 : FiniteDimensional ℝ V
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℂ E
f : V → E
inst_7 : CompleteSpace E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
h'f : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (𝓕 f) volume
v : V
hv : ContinuousAt f v
rw : 𝓕⁻ (𝓕 f) v = f v
⊢ 𝓕 (𝓕⁻ f) v = f v

Tactic:
rw [fourierInv_comm]

Premises used: Real.fourierInv_comm
-- Module: Mathlib.Analysis.Fourier.Inversion
Goal:
V : Type u_1
E : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MeasurableSpace V
inst_3 : BorelSpace V
inst_4 : FiniteDimensional ℝ V
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℂ E
f : V → E
inst_7 : CompleteSpace E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
h'f : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (𝓕 f) volume
v : V
hv : ContinuousAt f v
⊢ 𝓕⁻ (𝓕 f) v = f v

Tactic:
hf.fourierInv_fourier_eq h'f hv

Premises used: MeasureTheory.Integrable.fourierInv_fourier_eq
-- Module: Mathlib.Analysis.Fourier.Inversion
Goal:
V : Type u_1
E : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MeasurableSpace V
inst_3 : BorelSpace V
inst_4 : FiniteDimensional ℝ V
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℂ E
f : V → E
inst_7 : CompleteSpace E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
h'f : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (𝓕 f) volume
v : V
hv : ContinuousAt f v
⊢ 𝓕⁻ (𝓕 f) v = f v

Tactic:
exact hf.fourierInv_fourier_eq h'f hv

Premises used: MeasureTheory.Integrable.fourierInv_fourier_eq
-- Module: Mathlib.Analysis.Fourier.Inversion
Goal:
V : Type u_1
E : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MeasurableSpace V
inst_3 : BorelSpace V
inst_4 : FiniteDimensional ℝ V
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℂ E
f : V → E
inst_7 : CompleteSpace E
h :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
h'f : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (𝓕 f) volume
h₁ : ∀ (v : V), 𝓕 (𝓕⁻ f) v = f v
⊢ 𝓕 (𝓕⁻ f) = f

Tactic:
ext v
-- Module: Mathlib.Analysis.Fourier.Inversion
Goal:
V : Type u_1
E : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MeasurableSpace V
inst_3 : BorelSpace V
inst_4 : FiniteDimensional ℝ V
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℂ E
f : V → E
inst_7 : CompleteSpace E
h :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
h'f : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (𝓕 f) volume
v : V
⊢ 𝓕 (𝓕⁻ f) v = f v

Tactic:
hf.fourier_fourierInv_eq h'f h.continuousAt

Premises used: Continuous.continuousAt, MeasureTheory.Integrable.fourier_fourierInv_eq
-- Module: Mathlib.Analysis.Fourier.Inversion
Goal:
V : Type u_1
E : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MeasurableSpace V
inst_3 : BorelSpace V
inst_4 : FiniteDimensional ℝ V
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℂ E
f : V → E
inst_7 : CompleteSpace E
h :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
h'f : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (𝓕 f) volume
v : V
⊢ 𝓕 (𝓕⁻ f) v = f v

Tactic:
exact hf.fourier_fourierInv_eq h'f h.continuousAt

Premises used: Continuous.continuousAt, MeasureTheory.Integrable.fourier_fourierInv_eq
-- Module: Mathlib.Analysis.Fourier.LpSpace
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℂ F
inst_5 : CompleteSpace F
inst_6 : InnerProductSpace ℝ E
inst_7 : FiniteDimensional ℝ E
f : ↥(Lp F 2 volume)
⊢ ‖𝓕 f‖ = ‖f‖

Tactic:
(Lp.fourierTransformₗᵢ E F).norm_map f

Premises used: LinearIsometryEquiv.norm_map, ENNReal.toReal, MeasureTheory.Lp.fourierTransformₗᵢ, NNReal.toReal
-- Module: Mathlib.Analysis.Fourier.LpSpace
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℂ F
inst_5 : CompleteSpace F
inst_6 : InnerProductSpace ℝ E
inst_7 : FiniteDimensional ℝ E
f : ↥(Lp F 2 volume)
g : ↥(Lp F 2 volume)
⊢ ⟪𝓕 f, 𝓕 g⟫ = ⟪f, g⟫

Tactic:
(Lp.fourierTransformₗᵢ E F).inner_map_map f g

Premises used: LinearIsometryEquiv.inner_map_map, MeasureTheory.Lp.fourierTransformₗᵢ
-- Module: Mathlib.Analysis.Fourier.LpSpace
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℂ F
inst_5 : CompleteSpace F
inst_6 : InnerProductSpace ℝ E
inst_7 : FiniteDimensional ℝ E
f : 𝓢(E, F)
h_dense :
  DenseRange (X := ↥(Lp F 2 volume)) (α := 𝓢(E, F))
    (⇑(↑(toLpCLM ℂ F 2 volume) : 𝓢(E, F) →ₗ[ℂ] ↥(Lp F 2 volume)) : (a : 𝓢(E, F)) → ↥(Lp F 2 volume))
h_norm :
  ∃ (C : ℝ),
    ∀ (x : 𝓢(E, F)),
      norm (E := ↥(Lp F 2 volume))
          (((↑(toLpCLM ℂ F 2 volume) : 𝓢(E, F) →ₗ[ℂ] ↥(Lp F 2 volume)) ∘ₗ
                  (↑(fourierEquiv ℂ 𝓢(E, F)) : 𝓢(E, F) →ₗ[ℂ] 𝓢(E, F)) :
                (a : 𝓢(E, F)) → ↥(Lp F 2 volume))
              x :
            ↥(Lp F 2 volume)) ≤
        C *
          norm (E := ↥(Lp F 2 volume))
            (((↑(toLpCLM ℂ F 2 volume) : 𝓢(E, F) →ₗ[ℂ] ↥(Lp F 2 volume)) : (a : 𝓢(E, F)) → ↥(Lp F 2 volume)) x :
              ↥(Lp F 2 volume))
⊢ 𝓕 (E := ↥(Lp F 2 volume)) (f.toLp 2 volume) = (𝓕 f).toLp 2 volume

Tactic:
apply LinearMap.extendOfNorm_eq

Premises used: LinearMap.extendOfNorm_eq
-- Module: Mathlib.Analysis.Fourier.LpSpace
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℂ F
inst_5 : CompleteSpace F
inst_6 : InnerProductSpace ℝ E
inst_7 : FiniteDimensional ℝ E
f : 𝓢(E, F)
⊢ DenseRange (X := ↥(Lp F 2 volume)) (α := 𝓢(E, F))
    (⇑(↑(toLpCLM ℂ F 2 volume) : 𝓢(E, F) →ₗ[ℂ] ↥(Lp F 2 volume)) : (a : 𝓢(E, F)) → ↥(Lp F 2 volume))

Tactic:
SchwartzMap.denseRange_toLpCLM ENNReal.ofNat_ne_top

Premises used: ENNReal.ofNat_ne_top, Set.Mem, setOf, SchwartzMap.denseRange_toLpCLM
-- Module: Mathlib.Analysis.Fourier.LpSpace
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℂ F
inst_5 : CompleteSpace F
inst_6 : InnerProductSpace ℝ E
inst_7 : FiniteDimensional ℝ E
f : 𝓢(E, F)
⊢ DenseRange (X := ↥(Lp F 2 volume)) (α := 𝓢(E, F))
    (⇑(↑(toLpCLM ℂ F 2 volume) : 𝓢(E, F) →ₗ[ℂ] ↥(Lp F 2 volume)) : (a : 𝓢(E, F)) → ↥(Lp F 2 volume))

Tactic:
exact SchwartzMap.denseRange_toLpCLM ENNReal.ofNat_ne_top
-- Module: Mathlib.Analysis.Fourier.LpSpace
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℂ F
inst_5 : CompleteSpace F
inst_6 : InnerProductSpace ℝ E
inst_7 : FiniteDimensional ℝ E
f : 𝓢(E, F)
h :
  ∀ (x : 𝓢(E, F)),
    norm (E := ↥(Lp F 2 volume))
        (((↑(toLpCLM ℂ F 2 volume) : 𝓢(E, F) →ₗ[ℂ] ↥(Lp F 2 volume)) ∘ₗ
                (↑(fourierEquiv ℂ 𝓢(E, F)) : 𝓢(E, F) →ₗ[ℂ] 𝓢(E, F)) :
              (a : 𝓢(E, F)) → ↥(Lp F 2 volume))
            x :
          ↥(Lp F 2 volume)) ≤
      1 *
        norm (E := ↥(Lp F 2 volume))
          (((↑(toLpCLM ℂ F 2 volume) : 𝓢(E, F) →ₗ[ℂ] ↥(Lp F 2 volume)) : (a : 𝓢(E, F)) → ↥(Lp F 2 volume)) x :
            ↥(Lp F 2 volume))
⊢ ∃ (C : ℝ),
    ∀ (x : 𝓢(E, F)),
      norm (E := ↥(Lp F 2 volume))
          (((↑(toLpCLM ℂ F 2 volume) : 𝓢(E, F) →ₗ[ℂ] ↥(Lp F 2 volume)) ∘ₗ
                  (↑(fourierEquiv ℂ 𝓢(E, F)) : 𝓢(E, F) →ₗ[ℂ] 𝓢(E, F)) :
                (a : 𝓢(E, F)) → ↥(Lp F 2 volume))
              x :
            ↥(Lp F 2 volume)) ≤
        C *
          norm (E := ↥(Lp F 2 volume))
            (((↑(toLpCLM ℂ F 2 volume) : 𝓢(E, F) →ₗ[ℂ] ↥(Lp F 2 volume)) : (a : 𝓢(E, F)) → ↥(Lp F 2 volume)) x :
              ↥(Lp F 2 volume))

Tactic:
use 1
-- Module: Mathlib.Analysis.Fourier.LpSpace
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℂ F
inst_5 : CompleteSpace F
inst_6 : InnerProductSpace ℝ E
inst_7 : FiniteDimensional ℝ E
f_1 f : 𝓢(E, F)
h :
  norm (E := ↥(Lp F 2 volume))
      (((↑(toLpCLM ℂ F 2 volume) : 𝓢(E, F) →ₗ[ℂ] ↥(Lp F 2 volume)) ∘ₗ
              (↑(fourierEquiv ℂ 𝓢(E, F)) : 𝓢(E, F) →ₗ[ℂ] 𝓢(E, F)) :
            (a : 𝓢(E, F)) → ↥(Lp F 2 volume))
          f :
        ↥(Lp F 2 volume)) ≤
    norm (E := ↥(Lp F 2 volume))
      (((↑(toLpCLM ℂ F 2 volume) : 𝓢(E, F) →ₗ[ℂ] ↥(Lp F 2 volume)) : (a : 𝓢(E, F)) → ↥(Lp F 2 volume)) f :
        ↥(Lp F 2 volume))
⊢ norm (E := ↥(Lp F 2 volume))
      (((↑(toLpCLM ℂ F 2 volume) : 𝓢(E, F) →ₗ[ℂ] ↥(Lp F 2 volume)) ∘ₗ
              (↑(fourierEquiv ℂ 𝓢(E, F)) : 𝓢(E, F) →ₗ[ℂ] 𝓢(E, F)) :
            (a : 𝓢(E, F)) → ↥(Lp F 2 volume))
          f :
        ↥(Lp F 2 volume)) ≤
    1 *
      norm (E := ↥(Lp F 2 volume))
        (((↑(toLpCLM ℂ F 2 volume) : 𝓢(E, F) →ₗ[ℂ] ↥(Lp F 2 volume)) : (a : 𝓢(E, F)) → ↥(Lp F 2 volume)) f :
          ↥(Lp F 2 volume))

Tactic:
rw [one_mul]

Premises used: one_mul
-- Module: Mathlib.Analysis.Fourier.LpSpace
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℂ F
inst_5 : CompleteSpace F
inst_6 : InnerProductSpace ℝ E
inst_7 : FiniteDimensional ℝ E
f_1 f : 𝓢(E, F)
⊢ norm (E := ↥(Lp F 2 volume))
      (((↑(toLpCLM ℂ F 2 volume) : 𝓢(E, F) →ₗ[ℂ] ↥(Lp F 2 volume)) ∘ₗ
              (↑(fourierEquiv ℂ 𝓢(E, F)) : 𝓢(E, F) →ₗ[ℂ] 𝓢(E, F)) :
            (a : 𝓢(E, F)) → ↥(Lp F 2 volume))
          f :
        ↥(Lp F 2 volume)) ≤
    norm (E := ↥(Lp F 2 volume))
      (((↑(toLpCLM ℂ F 2 volume) : 𝓢(E, F) →ₗ[ℂ] ↥(Lp F 2 volume)) : (a : 𝓢(E, F)) → ↥(Lp F 2 volume)) f :
        ↥(Lp F 2 volume))

Tactic:
(norm_fourier_toL2_eq f).le

Premises used: SchwartzMap.norm_fourier_toL2_eq, Eq.le, ENNReal.toReal, NNReal.toReal
-- Module: Mathlib.Analysis.Fourier.LpSpace
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℂ F
inst_5 : CompleteSpace F
inst_6 : InnerProductSpace ℝ E
inst_7 : FiniteDimensional ℝ E
f_1 f : 𝓢(E, F)
⊢ norm (E := ↥(Lp F 2 volume))
      (((↑(toLpCLM ℂ F 2 volume) : 𝓢(E, F) →ₗ[ℂ] ↥(Lp F 2 volume)) ∘ₗ
              (↑(fourierEquiv ℂ 𝓢(E, F)) : 𝓢(E, F) →ₗ[ℂ] 𝓢(E, F)) :
            (a : 𝓢(E, F)) → ↥(Lp F 2 volume))
          f :
        ↥(Lp F 2 volume)) ≤
    norm (E := ↥(Lp F 2 volume))
      (((↑(toLpCLM ℂ F 2 volume) : 𝓢(E, F) →ₗ[ℂ] ↥(Lp F 2 volume)) : (a : 𝓢(E, F)) → ↥(Lp F 2 volume)) f :
        ↥(Lp F 2 volume))

Tactic:
exact (norm_fourier_toL2_eq f).le

Premises used: SchwartzMap.norm_fourier_toL2_eq, Eq.le
-- Module: Mathlib.Analysis.Fourier.LpSpace
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℂ F
inst_5 : CompleteSpace F
inst_6 : InnerProductSpace ℝ E
inst_7 : FiniteDimensional ℝ E
f : 𝓢(E, F)
h_dense :
  DenseRange (X := ↥(Lp F 2 volume)) (α := 𝓢(E, F))
    (⇑(↑(toLpCLM ℂ F 2 volume) : 𝓢(E, F) →ₗ[ℂ] ↥(Lp F 2 volume)) : (a : 𝓢(E, F)) → ↥(Lp F 2 volume))
h_norm :
  ∃ (C : ℝ),
    ∀ (x : 𝓢(E, F)),
      norm (E := ↥(Lp F 2 volume))
          (((↑(toLpCLM ℂ F 2 volume) : 𝓢(E, F) →ₗ[ℂ] ↥(Lp F 2 volume)) ∘ₗ
                  (↑(LinearEquiv.symm (fourierEquiv ℂ 𝓢(E, F))) : 𝓢(E, F) →ₗ[ℂ] 𝓢(E, F)) :
                (a : 𝓢(E, F)) → ↥(Lp F 2 volume))
              x :
            ↥(Lp F 2 volume)) ≤
        C *
          norm (E := ↥(Lp F 2 volume))
            (((↑(toLpCLM ℂ F 2 volume) : 𝓢(E, F) →ₗ[ℂ] ↥(Lp F 2 volume)) : (a : 𝓢(E, F)) → ↥(Lp F 2 volume)) x :
              ↥(Lp F 2 volume))
⊢ 𝓕⁻ (E := ↥(Lp F 2 volume)) (f.toLp 2 volume) = (𝓕⁻ f).toLp 2 volume

Tactic:
apply LinearMap.extendOfNorm_eq

Premises used: LinearMap.extendOfNorm_eq
-- Module: Mathlib.Analysis.Fourier.LpSpace
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℂ F
inst_5 : CompleteSpace F
inst_6 : InnerProductSpace ℝ E
inst_7 : FiniteDimensional ℝ E
f : 𝓢(E, F)
h :
  ∀ (x : 𝓢(E, F)),
    norm (E := ↥(Lp F 2 volume))
        (((↑(toLpCLM ℂ F 2 volume) : 𝓢(E, F) →ₗ[ℂ] ↥(Lp F 2 volume)) ∘ₗ
                (↑(LinearEquiv.symm (fourierEquiv ℂ 𝓢(E, F))) : 𝓢(E, F) →ₗ[ℂ] 𝓢(E, F)) :
              (a : 𝓢(E, F)) → ↥(Lp F 2 volume))
            x :
          ↥(Lp F 2 volume)) ≤
      1 *
        norm (E := ↥(Lp F 2 volume))
          (((↑(toLpCLM ℂ F 2 volume) : 𝓢(E, F) →ₗ[ℂ] ↥(Lp F 2 volume)) : (a : 𝓢(E, F)) → ↥(Lp F 2 volume)) x :
            ↥(Lp F 2 volume))
⊢ ∃ (C : ℝ),
    ∀ (x : 𝓢(E, F)),
      norm (E := ↥(Lp F 2 volume))
          (((↑(toLpCLM ℂ F 2 volume) : 𝓢(E, F) →ₗ[ℂ] ↥(Lp F 2 volume)) ∘ₗ
                  (↑(LinearEquiv.symm (fourierEquiv ℂ 𝓢(E, F))) : 𝓢(E, F) →ₗ[ℂ] 𝓢(E, F)) :
                (a : 𝓢(E, F)) → ↥(Lp F 2 volume))
              x :
            ↥(Lp F 2 volume)) ≤
        C *
          norm (E := ↥(Lp F 2 volume))
            (((↑(toLpCLM ℂ F 2 volume) : 𝓢(E, F) →ₗ[ℂ] ↥(Lp F 2 volume)) : (a : 𝓢(E, F)) → ↥(Lp F 2 volume)) x :
              ↥(Lp F 2 volume))

Tactic:
use 1
-- Module: Mathlib.Analysis.Fourier.LpSpace
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℂ F
inst_5 : CompleteSpace F
inst_6 : InnerProductSpace ℝ E
inst_7 : FiniteDimensional ℝ E
f_1 f : 𝓢(E, F)
h :
  norm (E := ↥(Lp F 2 volume))
      (((↑(toLpCLM ℂ F 2 volume) : 𝓢(E, F) →ₗ[ℂ] ↥(Lp F 2 volume)) ∘ₗ
              (↑(LinearEquiv.symm (fourierEquiv ℂ 𝓢(E, F))) : 𝓢(E, F) →ₗ[ℂ] 𝓢(E, F)) :
            (a : 𝓢(E, F)) → ↥(Lp F 2 volume))
          f :
        ↥(Lp F 2 volume)) ≤
    norm (E := ↥(Lp F 2 volume))
      (((↑(toLpCLM ℂ F 2 volume) : 𝓢(E, F) →ₗ[ℂ] ↥(Lp F 2 volume)) : (a : 𝓢(E, F)) → ↥(Lp F 2 volume)) f :
        ↥(Lp F 2 volume))
⊢ norm (E := ↥(Lp F 2 volume))
      (((↑(toLpCLM ℂ F 2 volume) : 𝓢(E, F) →ₗ[ℂ] ↥(Lp F 2 volume)) ∘ₗ
              (↑(LinearEquiv.symm (fourierEquiv ℂ 𝓢(E, F))) : 𝓢(E, F) →ₗ[ℂ] 𝓢(E, F)) :
            (a : 𝓢(E, F)) → ↥(Lp F 2 volume))
          f :
        ↥(Lp F 2 volume)) ≤
    1 *
      norm (E := ↥(Lp F 2 volume))
        (((↑(toLpCLM ℂ F 2 volume) : 𝓢(E, F) →ₗ[ℂ] ↥(Lp F 2 volume)) : (a : 𝓢(E, F)) → ↥(Lp F 2 volume)) f :
          ↥(Lp F 2 volume))

Tactic:
rw [one_mul]

Premises used: one_mul
-- Module: Mathlib.Analysis.Fourier.LpSpace
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℂ F
inst_5 : CompleteSpace F
inst_6 : InnerProductSpace ℝ E
inst_7 : FiniteDimensional ℝ E
f_1 f : 𝓢(E, F)
⊢ norm (E := ↥(Lp F 2 volume)) ((𝓕⁻ f).toLp 2 volume) ≤ norm (E := ↥(Lp F 2 volume)) ((𝓕 (𝓕⁻ f)).toLp 2 volume)

Tactic:
(norm_fourier_toL2_eq (𝓕⁻ f)).symm.le

Premises used: SchwartzMap.norm_fourier_toL2_eq, Eq.le, FourierTransformInv.fourierInv, Eq.symm
-- Module: Mathlib.Analysis.Fourier.LpSpace
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℂ F
inst_5 : CompleteSpace F
inst_6 : InnerProductSpace ℝ E
inst_7 : FiniteDimensional ℝ E
f_1 f : 𝓢(E, F)
h :
  Eq (α := ↥(Lp F 2 volume))
    (((↑(toLpCLM ℂ F 2 volume) : 𝓢(E, F) →ₗ[ℂ] ↥(Lp F 2 volume)) : (a : 𝓢(E, F)) → ↥(Lp F 2 volume)) f :
      ↥(Lp F 2 volume))
    ((𝓕 (𝓕⁻ f)).toLp 2 volume : ↥(Lp F 2 volume))
⊢ norm (E := ↥(Lp F 2 volume))
      (((↑(toLpCLM ℂ F 2 volume) : 𝓢(E, F) →ₗ[ℂ] ↥(Lp F 2 volume)) ∘ₗ
              (↑(LinearEquiv.symm (fourierEquiv ℂ 𝓢(E, F))) : 𝓢(E, F) →ₗ[ℂ] 𝓢(E, F)) :
            (a : 𝓢(E, F)) → ↥(Lp F 2 volume))
          f :
        ↥(Lp F 2 volume)) ≤
    norm (E := ↥(Lp F 2 volume))
      (((↑(toLpCLM ℂ F 2 volume) : 𝓢(E, F) →ₗ[ℂ] ↥(Lp F 2 volume)) : (a : 𝓢(E, F)) → ↥(Lp F 2 volume)) f :
        ↥(Lp F 2 volume))

Tactic:
convert! (norm_fourier_toL2_eq (𝓕⁻ f)).symm.le

Premises used: SchwartzMap.norm_fourier_toL2_eq, Eq.le, FourierTransformInv.fourierInv, Eq.symm
-- Module: Mathlib.Analysis.Fourier.LpSpace
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℂ F
inst_5 : CompleteSpace F
inst_6 : InnerProductSpace ℝ E
inst_7 : FiniteDimensional ℝ E
f_1 f : 𝓢(E, F)
⊢ Eq (α := ↥(Lp F 2 volume))
    (((↑(toLpCLM ℂ F 2 volume) : 𝓢(E, F) →ₗ[ℂ] ↥(Lp F 2 volume)) : (a : 𝓢(E, F)) → ↥(Lp F 2 volume)) f :
      ↥(Lp F 2 volume))
    ((𝓕 (𝓕⁻ f)).toLp 2 volume : ↥(Lp F 2 volume))

Tactic:
simp