internlm/Lean-Github huggingface dataset:
Theorem: IsBump.integrable
Proof state before:
case hf
α : Type u_1
inst✝⁴ : NormedAddCommGroup α
inst✝³ : NormedSpace ℝ α
inst✝² : MeasurableSpace α
inst✝¹ : OpensMeasurableSpace α
f : α → ℝ
hf : IsBump f
μ : autoParam (Measure α) _auto✝
inst✝ : IsLocallyFiniteMeasure μ
⊢ Continuous f

case hcf
α : Type u_1
inst✝⁴ : NormedAddCommGroup α
inst✝³ : NormedSpace ℝ α
inst✝² : MeasurableSpace α
inst✝¹ : OpensMeasurableSpace α
f : α → ℝ
hf : IsBump f
μ : autoParam (Measure α) _auto✝
inst✝ : IsLocallyFiniteMeasure μ
⊢ HasCompactSupport f
Tactic:
. exact ContDiff.continuous hf.right
Proof state after:
case hcf
α : Type u_1
inst✝⁴ : NormedAddCommGroup α
inst✝³ : NormedSpace ℝ α
inst✝² : MeasurableSpace α
inst✝¹ : OpensMeasurableSpace α
f : α → ℝ
hf : IsBump f
μ : autoParam (Measure α) _auto✝
inst✝ : IsLocallyFiniteMeasure μ
⊢ HasCompactSupport f
Theorem: IsBump.integrable
Proof state before:
case hcf
α : Type u_1
inst✝⁴ : NormedAddCommGroup α
inst✝³ : NormedSpace ℝ α
inst✝² : MeasurableSpace α
inst✝¹ : OpensMeasurableSpace α
f : α → ℝ
hf : IsBump f
μ : autoParam (Measure α) _auto✝
inst✝ : IsLocallyFiniteMeasure μ
⊢ HasCompactSupport f
Tactic:
. exact hf.left
Proof state after:
no goals
Theorem: IsBump.integrable
Proof state before:
case hf
α : Type u_1
inst✝⁴ : NormedAddCommGroup α
inst✝³ : NormedSpace ℝ α
inst✝² : MeasurableSpace α
inst✝¹ : OpensMeasurableSpace α
f : α → ℝ
hf : IsBump f
μ : autoParam (Measure α) _auto✝
inst✝ : IsLocallyFiniteMeasure μ
⊢ Continuous f
Tactic:
exact ContDiff.continuous hf.right
Proof state after:
no goals
Theorem: IsBump.integrable
Proof state before:
case hcf
α : Type u_1
inst✝⁴ : NormedAddCommGroup α
inst✝³ : NormedSpace ℝ α
inst✝² : MeasurableSpace α
inst✝¹ : OpensMeasurableSpace α
f : α → ℝ
hf : IsBump f
μ : autoParam (Measure α) _auto✝
inst✝ : IsLocallyFiniteMeasure μ
⊢ HasCompactSupport f
Tactic:
exact hf.left
Proof state after:
no goals
Theorem: IsBump.memL1
Proof state before:
α : Type u_1
inst✝⁴ : NormedAddCommGroup α
inst✝³ : NormedSpace ℝ α
inst✝² : MeasurableSpace α
inst✝¹ : OpensMeasurableSpace α
f : α → ℝ
hf : IsBump f
μ : autoParam (Measure α) _auto✝
inst✝ : IsLocallyFiniteMeasure μ
⊢ Memℒp f 1
Tactic:
simp [Memℒp]
Proof state after:
α : Type u_1
inst✝⁴ : NormedAddCommGroup α
inst✝³ : NormedSpace ℝ α
inst✝² : MeasurableSpace α
inst✝¹ : OpensMeasurableSpace α
f : α → ℝ
hf : IsBump f
μ : autoParam (Measure α) _auto✝
inst✝ : IsLocallyFiniteMeasure μ
⊢ AEStronglyMeasurable f μ ∧ snorm f 1 μ < ⊤
Theorem: IsBump.memL1
Proof state before:
α : Type u_1
inst✝⁴ : NormedAddCommGroup α
inst✝³ : NormedSpace ℝ α
inst✝² : MeasurableSpace α
inst✝¹ : OpensMeasurableSpace α
f : α → ℝ
hf : IsBump f
μ : autoParam (Measure α) _auto✝
inst✝ : IsLocallyFiniteMeasure μ
⊢ AEStronglyMeasurable f μ ∧ snorm f 1 μ < ⊤
Tactic:
apply And.intro
Proof state after:
case left
α : Type u_1
inst✝⁴ : NormedAddCommGroup α
inst✝³ : NormedSpace ℝ α
inst✝² : MeasurableSpace α
inst✝¹ : OpensMeasurableSpace α
f : α → ℝ
hf : IsBump f
μ : autoParam (Measure α) _auto✝
inst✝ : IsLocallyFiniteMeasure μ
⊢ AEStronglyMeasurable f μ

case right
α : Type u_1
inst✝⁴ : NormedAddCommGroup α
inst✝³ : NormedSpace ℝ α
inst✝² : MeasurableSpace α
inst✝¹ : OpensMeasurableSpace α
f : α → ℝ
hf : IsBump f
μ : autoParam (Measure α) _auto✝
inst✝ : IsLocallyFiniteMeasure μ
⊢ snorm f 1 μ < ⊤
Theorem: IsBump.memL1
Proof state before:
case left
α : Type u_1
inst✝⁴ : NormedAddCommGroup α
inst✝³ : NormedSpace ℝ α
inst✝² : MeasurableSpace α
inst✝¹ : OpensMeasurableSpace α
f : α → ℝ
hf : IsBump f
μ : autoParam (Measure α) _auto✝
inst✝ : IsLocallyFiniteMeasure μ
⊢ AEStronglyMeasurable f μ

case right
α : Type u_1
inst✝⁴ : NormedAddCommGroup α
inst✝³ : NormedSpace ℝ α
inst✝² : MeasurableSpace α
inst✝¹ : OpensMeasurableSpace α
f : α → ℝ
hf : IsBump f
μ : autoParam (Measure α) _auto✝
inst✝ : IsLocallyFiniteMeasure μ
⊢ snorm f 1 μ < ⊤
Tactic:
. exact aestronglyMeasurable hf μ
Proof state after:
case right
α : Type u_1
inst✝⁴ : NormedAddCommGroup α
inst✝³ : NormedSpace ℝ α
inst✝² : MeasurableSpace α
inst✝¹ : OpensMeasurableSpace α
f : α → ℝ
hf : IsBump f
μ : autoParam (Measure α) _auto✝
inst✝ : IsLocallyFiniteMeasure μ
⊢ snorm f 1 μ < ⊤
Theorem: IsBump.memL1
Proof state before:
case right
α : Type u_1
inst✝⁴ : NormedAddCommGroup α
inst✝³ : NormedSpace ℝ α
inst✝² : MeasurableSpace α
inst✝¹ : OpensMeasurableSpace α
f : α → ℝ
hf : IsBump f
μ : autoParam (Measure α) _auto✝
inst✝ : IsLocallyFiniteMeasure μ
⊢ snorm f 1 μ < ⊤
Tactic:
. simp [snorm, snorm']
  exact (integrable hf μ).right
Proof state after:
no goals
Theorem: IsBump.memL1
Proof state before:
case left
α : Type u_1
inst✝⁴ : NormedAddCommGroup α
inst✝³ : NormedSpace ℝ α
inst✝² : MeasurableSpace α
inst✝¹ : OpensMeasurableSpace α
f : α → ℝ
hf : IsBump f
μ : autoParam (Measure α) _auto✝
inst✝ : IsLocallyFiniteMeasure μ
⊢ AEStronglyMeasurable f μ
Tactic:
exact aestronglyMeasurable hf μ
Proof state after:
no goals
Theorem: IsBump.memL1
Proof state before:
case right
α : Type u_1
inst✝⁴ : NormedAddCommGroup α
inst✝³ : NormedSpace ℝ α
inst✝² : MeasurableSpace α
inst✝¹ : OpensMeasurableSpace α
f : α → ℝ
hf : IsBump f
μ : autoParam (Measure α) _auto✝
inst✝ : IsLocallyFiniteMeasure μ
⊢ snorm f 1 μ < ⊤
Tactic:
simp [snorm, snorm']
Proof state after:
case right
α : Type u_1
inst✝⁴ : NormedAddCommGroup α
inst✝³ : NormedSpace ℝ α
inst✝² : MeasurableSpace α
inst✝¹ : OpensMeasurableSpace α
f : α → ℝ
hf : IsBump f
μ : autoParam (Measure α) _auto✝
inst✝ : IsLocallyFiniteMeasure μ
⊢ ∫⁻ (a : α), ↑‖f a‖₊ ∂μ < ⊤
Theorem: IsBump.memL1
Proof state before:
case right
α : Type u_1
inst✝⁴ : NormedAddCommGroup α
inst✝³ : NormedSpace ℝ α
inst✝² : MeasurableSpace α
inst✝¹ : OpensMeasurableSpace α
f : α → ℝ
hf : IsBump f
μ : autoParam (Measure α) _auto✝
inst✝ : IsLocallyFiniteMeasure μ
⊢ ∫⁻ (a : α), ↑‖f a‖₊ ∂μ < ⊤
Tactic:
exact (integrable hf μ).right
Proof state after:
no goals
Theorem: IsBump.integrable_mul_continuous
Proof state before:
α : Type u_1
inst✝⁴ : NormedAddCommGroup α
inst✝³ : NormedSpace ℝ α
inst✝² : MeasurableSpace α
inst✝¹ : OpensMeasurableSpace α
f✝ : α → ℝ
hf✝ : IsBump f✝
f g : α → ℝ
hf : IsBump f
hg : Continuous g
μ : autoParam (Measure α) _auto✝
inst✝ : IsLocallyFiniteMeasure μ
⊢ Integrable (f * g)
Tactic:
apply Continuous.integrable_of_hasCompactSupport
Proof state after:
case hf
α : Type u_1
inst✝⁴ : NormedAddCommGroup α
inst✝³ : NormedSpace ℝ α
inst✝² : MeasurableSpace α
inst✝¹ : OpensMeasurableSpace α
f✝ : α → ℝ
hf✝ : IsBump f✝
f g : α → ℝ
hf : IsBump f
hg : Continuous g
μ : autoParam (Measure α) _auto✝
inst✝ : IsLocallyFiniteMeasure μ
⊢ Continuous (f * g)

case hcf
α : Type u_1
inst✝⁴ : NormedAddCommGroup α
inst✝³ : NormedSpace ℝ α
inst✝² : MeasurableSpace α
inst✝¹ : OpensMeasurableSpace α
f✝ : α → ℝ
hf✝ : IsBump f✝
f g : α → ℝ
hf : IsBump f
hg : Continuous g
μ : autoParam (Measure α) _auto✝
inst✝ : IsLocallyFiniteMeasure μ
⊢ HasCompactSupport (f * g)
Theorem: IsBump.integrable_mul_continuous
Proof state before:
case hf
α : Type u_1
inst✝⁴ : NormedAddCommGroup α
inst✝³ : NormedSpace ℝ α
inst✝² : MeasurableSpace α
inst✝¹ : OpensMeasurableSpace α
f✝ : α → ℝ
hf✝ : IsBump f✝
f g : α → ℝ
hf : IsBump f
hg : Continuous g
μ : autoParam (Measure α) _auto✝
inst✝ : IsLocallyFiniteMeasure μ
⊢ Continuous (f * g)

case hcf
α : Type u_1
inst✝⁴ : NormedAddCommGroup α
inst✝³ : NormedSpace ℝ α
inst✝² : MeasurableSpace α
inst✝¹ : OpensMeasurableSpace α
f✝ : α → ℝ
hf✝ : IsBump f✝
f g : α → ℝ
hf : IsBump f
hg : Continuous g
μ : autoParam (Measure α) _auto✝
inst✝ : IsLocallyFiniteMeasure μ
⊢ HasCompactSupport (f * g)
Tactic:
. exact Continuous.mul hf.continuous hg
Proof state after:
case hcf
α : Type u_1
inst✝⁴ : NormedAddCommGroup α
inst✝³ : NormedSpace ℝ α
inst✝² : MeasurableSpace α
inst✝¹ : OpensMeasurableSpace α
f✝ : α → ℝ
hf✝ : IsBump f✝
f g : α → ℝ
hf : IsBump f
hg : Continuous g
μ : autoParam (Measure α) _auto✝
inst✝ : IsLocallyFiniteMeasure μ
⊢ HasCompactSupport (f * g)
Theorem: IsBump.integrable_mul_continuous
Proof state before:
case hcf
α : Type u_1
inst✝⁴ : NormedAddCommGroup α
inst✝³ : NormedSpace ℝ α
inst✝² : MeasurableSpace α
inst✝¹ : OpensMeasurableSpace α
f✝ : α → ℝ
hf✝ : IsBump f✝
f g : α → ℝ
hf : IsBump f
hg : Continuous g
μ : autoParam (Measure α) _auto✝
inst✝ : IsLocallyFiniteMeasure μ
⊢ HasCompactSupport (f * g)
Tactic:
. apply HasCompactSupport.mul_right hf.left
Proof state after:
no goals
Theorem: IsBump.integrable_mul_continuous
Proof state before:
case hf
α : Type u_1
inst✝⁴ : NormedAddCommGroup α
inst✝³ : NormedSpace ℝ α
inst✝² : MeasurableSpace α
inst✝¹ : OpensMeasurableSpace α
f✝ : α → ℝ
hf✝ : IsBump f✝
f g : α → ℝ
hf : IsBump f
hg : Continuous g
μ : autoParam (Measure α) _auto✝
inst✝ : IsLocallyFiniteMeasure μ
⊢ Continuous (f * g)
Tactic:
exact Continuous.mul hf.continuous hg
Proof state after:
no goals
Theorem: IsBump.integrable_mul_continuous
Proof state before:
case hcf
α : Type u_1
inst✝⁴ : NormedAddCommGroup α
inst✝³ : NormedSpace ℝ α
inst✝² : MeasurableSpace α
inst✝¹ : OpensMeasurableSpace α
f✝ : α → ℝ
hf✝ : IsBump f✝
f g : α → ℝ
hf : IsBump f
hg : Continuous g
μ : autoParam (Measure α) _auto✝
inst✝ : IsLocallyFiniteMeasure μ
⊢ HasCompactSupport (f * g)
Tactic:
apply HasCompactSupport.mul_right hf.left
Proof state after:
no goals
Theorem: IsBump.integrable_continuous_mul
Proof state before:
α : Type u_1
inst✝⁴ : NormedAddCommGroup α
inst✝³ : NormedSpace ℝ α
inst✝² : MeasurableSpace α
inst✝¹ : OpensMeasurableSpace α
f✝ : α → ℝ
hf✝ : IsBump f✝
f g : α → ℝ
hf : Continuous f
hg : IsBump g
μ : autoParam (Measure α) _auto✝
inst✝ : IsLocallyFiniteMeasure μ
⊢ Integrable (f * g)
Tactic:
rw [mul_comm]
Proof state after:
α : Type u_1
inst✝⁴ : NormedAddCommGroup α
inst✝³ : NormedSpace ℝ α
inst✝² : MeasurableSpace α
inst✝¹ : OpensMeasurableSpace α
f✝ : α → ℝ
hf✝ : IsBump f✝
f g : α → ℝ
hf : Continuous f
hg : IsBump g
μ : autoParam (Measure α) _auto✝
inst✝ : IsLocallyFiniteMeasure μ
⊢ Integrable (g * f)
Theorem: IsBump.integrable_continuous_mul
Proof state before:
α : Type u_1
inst✝⁴ : NormedAddCommGroup α
inst✝³ : NormedSpace ℝ α
inst✝² : MeasurableSpace α
inst✝¹ : OpensMeasurableSpace α
f✝ : α → ℝ
hf✝ : IsBump f✝
f g : α → ℝ
hf : Continuous f
hg : IsBump g
μ : autoParam (Measure α) _auto✝
inst✝ : IsLocallyFiniteMeasure μ
⊢ Integrable (g * f)
Tactic:
apply integrable_mul_continuous <;> assumption
Proof state after:
no goals
Theorem: Real.fourierIntegral_continuous
Proof state before:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℝ → F
hf : Integrable f
⊢ Continuous fun p => ((LinearMap.mul ℝ ℝ) p.1) p.2
Tactic:
exact continuous_mul
Proof state after:
no goals
Theorem: RealVectorFourier.fourierIntegral_euclidean_eq_fourierIntegral_l2inner
Proof state before:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝⁸ : Fintype ι
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : MeasurableSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : CompleteSpace F
f : EuclideanSpace ℝ ι → F
ξ : EuclideanSpace ℝ ι
⊢ 𝓕ᵥ f ξ = 𝓕ₙ f ξ
Tactic:
rw [VectorFourier.fourierIntegral]
Proof state after:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝⁸ : Fintype ι
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : MeasurableSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : CompleteSpace F
f : EuclideanSpace ℝ ι → F
ξ : EuclideanSpace ℝ ι
⊢ ∫ (v : EuclideanSpace ℝ ι), ↑(Real.fourierChar (Multiplicative.ofAdd (-((innerₛₗ ℝ) v) ξ))) • f v = 𝓕ₙ f ξ
Theorem: RealVectorFourier.fourierIntegral_euclidean_eq_fourierIntegral_l2inner
Proof state before:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝⁸ : Fintype ι
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : MeasurableSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : CompleteSpace F
f : EuclideanSpace ℝ ι → F
ξ : EuclideanSpace ℝ ι
⊢ ∫ (v : EuclideanSpace ℝ ι), ↑(Real.fourierChar (Multiplicative.ofAdd (-((innerₛₗ ℝ) v) ξ))) • f v = 𝓕ₙ f ξ
Tactic:
rw [← MeasurePreserving.integral_comp' (EuclideanSpace.volume_preserving_measurableEquiv ι).symm]
Proof state after:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝⁸ : Fintype ι
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : MeasurableSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : CompleteSpace F
f : EuclideanSpace ℝ ι → F
ξ : EuclideanSpace ℝ ι
⊢ ∫ (x : ι → ℝ),
      ↑(Real.fourierChar (Multiplicative.ofAdd (-((innerₛₗ ℝ) ((EuclideanSpace.measurableEquiv ι).symm x)) ξ))) •
        f ((EuclideanSpace.measurableEquiv ι).symm x) ∂volume =
    𝓕ₙ f ξ
Theorem: RealVectorFourier.fourierIntegral_euclidean_eq_fourierIntegral_l2inner
Proof state before:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝⁸ : Fintype ι
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : MeasurableSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : CompleteSpace F
f : EuclideanSpace ℝ ι → F
ξ : EuclideanSpace ℝ ι
⊢ ∫ (x : ι → ℝ),
      ↑(Real.fourierChar (Multiplicative.ofAdd (-((innerₛₗ ℝ) ((EuclideanSpace.measurableEquiv ι).symm x)) ξ))) •
        f ((EuclideanSpace.measurableEquiv ι).symm x) ∂volume =
    𝓕ₙ f ξ
Tactic:
rfl
Proof state after:
no goals
Theorem: RealVectorFourier.fourierIntegral_l2inner_eq_fourierIntegral_euclidean
Proof state before:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝⁸ : Fintype ι
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : MeasurableSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : CompleteSpace F
f : (ι → ℝ) → F
ξ : ι → ℝ
⊢ 𝓕ₙ f ξ = 𝓕ᵥ (f ∘ ⇑(EuclideanSpace.equiv ι ℝ)) ξ
Tactic:
rw [VectorFourier.fourierIntegral]
Proof state after:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝⁸ : Fintype ι
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : MeasurableSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : CompleteSpace F
f : (ι → ℝ) → F
ξ : ι → ℝ
⊢ ∫ (v : ι → ℝ), ↑(Real.fourierChar (Multiplicative.ofAdd (-((l2innerₛₗ ℝ) v) ξ))) • f v =
    𝓕ᵥ (f ∘ ⇑(EuclideanSpace.equiv ι ℝ)) ξ
Theorem: RealVectorFourier.fourierIntegral_l2inner_eq_fourierIntegral_euclidean
Proof state before:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝⁸ : Fintype ι
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : MeasurableSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : CompleteSpace F
f : (ι → ℝ) → F
ξ : ι → ℝ
⊢ ∫ (v : ι → ℝ), ↑(Real.fourierChar (Multiplicative.ofAdd (-((l2innerₛₗ ℝ) v) ξ))) • f v =
    𝓕ᵥ (f ∘ ⇑(EuclideanSpace.equiv ι ℝ)) ξ
Tactic:
rw [← MeasurePreserving.integral_comp' (EuclideanSpace.volume_preserving_measurableEquiv ι)]
Proof state after:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝⁸ : Fintype ι
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : MeasurableSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : CompleteSpace F
f : (ι → ℝ) → F
ξ : ι → ℝ
⊢ ∫ (x : EuclideanSpace ℝ ι),
      ↑(Real.fourierChar (Multiplicative.ofAdd (-((l2innerₛₗ ℝ) ((EuclideanSpace.measurableEquiv ι) x)) ξ))) •
        f ((EuclideanSpace.measurableEquiv ι) x) ∂volume =
    𝓕ᵥ (f ∘ ⇑(EuclideanSpace.equiv ι ℝ)) ξ
Theorem: RealVectorFourier.fourierIntegral_l2inner_eq_fourierIntegral_euclidean
Proof state before:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝⁸ : Fintype ι
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : MeasurableSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : CompleteSpace F
f : (ι → ℝ) → F
ξ : ι → ℝ
⊢ ∫ (x : EuclideanSpace ℝ ι),
      ↑(Real.fourierChar (Multiplicative.ofAdd (-((l2innerₛₗ ℝ) ((EuclideanSpace.measurableEquiv ι) x)) ξ))) •
        f ((EuclideanSpace.measurableEquiv ι) x) ∂volume =
    𝓕ᵥ (f ∘ ⇑(EuclideanSpace.equiv ι ℝ)) ξ
Tactic:
rfl
Proof state after:
no goals
Theorem: RealVectorFourier.fourierIntegral_eq_fourierIntegral_euclidean_ofOrthonormalBasis
Proof state before:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝⁸ : Fintype ι
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : MeasurableSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : CompleteSpace F
v : OrthonormalBasis ι ℝ E
f : E → F
ξ : E
⊢ 𝓕ᵥ f ξ = 𝓕ᵥ (f ∘ ⇑(LinearIsometryEquiv.symm v.repr)) (v.repr ξ)
Tactic:
rw [VectorFourier.fourierIntegral]
Proof state after:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝⁸ : Fintype ι
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : MeasurableSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : CompleteSpace F
v : OrthonormalBasis ι ℝ E
f : E → F
ξ : E
⊢ ∫ (v : E), ↑(Real.fourierChar (Multiplicative.ofAdd (-((innerₛₗ ℝ) v) ξ))) • f v =
    𝓕ᵥ (f ∘ ⇑(LinearIsometryEquiv.symm v.repr)) (v.repr ξ)
Theorem: RealVectorFourier.fourierIntegral_eq_fourierIntegral_euclidean_ofOrthonormalBasis
Proof state before:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝⁸ : Fintype ι
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : MeasurableSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : CompleteSpace F
v : OrthonormalBasis ι ℝ E
f : E → F
ξ : E
⊢ ∫ (v : E), ↑(Real.fourierChar (Multiplicative.ofAdd (-((innerₛₗ ℝ) v) ξ))) • f v =
    𝓕ᵥ (f ∘ ⇑(LinearIsometryEquiv.symm v.repr)) (v.repr ξ)
Tactic:
rw [VectorFourier.fourierIntegral]
Proof state after:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝⁸ : Fintype ι
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : MeasurableSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : CompleteSpace F
v : OrthonormalBasis ι ℝ E
f : E → F
ξ : E
⊢ ∫ (v : E), ↑(Real.fourierChar (Multiplicative.ofAdd (-((innerₛₗ ℝ) v) ξ))) • f v =
    ∫ (v_1 : EuclideanSpace ℝ ι),
      ↑(Real.fourierChar (Multiplicative.ofAdd (-((innerₛₗ ℝ) v_1) (v.repr ξ)))) •
        (f ∘ ⇑(LinearIsometryEquiv.symm v.repr)) v_1
Theorem: RealVectorFourier.fourierIntegral_eq_fourierIntegral_euclidean_ofOrthonormalBasis
Proof state before:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝⁸ : Fintype ι
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : MeasurableSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : CompleteSpace F
v : OrthonormalBasis ι ℝ E
f : E → F
ξ : E
⊢ ∫ (v : E), ↑(Real.fourierChar (Multiplicative.ofAdd (-((innerₛₗ ℝ) v) ξ))) • f v =
    ∫ (v_1 : EuclideanSpace ℝ ι),
      ↑(Real.fourierChar (Multiplicative.ofAdd (-((innerₛₗ ℝ) v_1) (v.repr ξ)))) •
        (f ∘ ⇑(LinearIsometryEquiv.symm v.repr)) v_1
Tactic:
rw [← MeasurePreserving.integral_comp' (v.measurePreserving_measurableEquiv)]
Proof state after:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝⁸ : Fintype ι
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : MeasurableSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : CompleteSpace F
v : OrthonormalBasis ι ℝ E
f : E → F
ξ : E
⊢ ∫ (v : E), ↑(Real.fourierChar (Multiplicative.ofAdd (-((innerₛₗ ℝ) v) ξ))) • f v =
    ∫ (x : E),
      ↑(Real.fourierChar (Multiplicative.ofAdd (-((innerₛₗ ℝ) ((OrthonormalBasis.measurableEquiv v) x)) (v.repr ξ)))) •
        (f ∘ ⇑(LinearIsometryEquiv.symm v.repr)) ((OrthonormalBasis.measurableEquiv v) x)
Theorem: RealVectorFourier.fourierIntegral_eq_fourierIntegral_euclidean_ofOrthonormalBasis
Proof state before:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝⁸ : Fintype ι
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : MeasurableSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : CompleteSpace F
v : OrthonormalBasis ι ℝ E
f : E → F
ξ : E
⊢ ∫ (v : E), ↑(Real.fourierChar (Multiplicative.ofAdd (-((innerₛₗ ℝ) v) ξ))) • f v =
    ∫ (x : E),
      ↑(Real.fourierChar (Multiplicative.ofAdd (-((innerₛₗ ℝ) ((OrthonormalBasis.measurableEquiv v) x)) (v.repr ξ)))) •
        (f ∘ ⇑(LinearIsometryEquiv.symm v.repr)) ((OrthonormalBasis.measurableEquiv v) x)
Tactic:
conv =>
  rhs; arg 2; intro x
  change Real.fourierChar[-innerₛₗ ℝ (v.repr x) (v.repr ξ)] • f (v.repr.symm (v.repr x))
  simp
Proof state after:
no goals
Theorem: RealVectorFourier.fourierIntegral_eq_fourierIntegral_l2inner_ofOrthonormalBasis
Proof state before:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝⁸ : Fintype ι
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : MeasurableSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : CompleteSpace F
v : OrthonormalBasis ι ℝ E
f : E → F
ξ : E
⊢ 𝓕ᵥ f ξ = 𝓕ₙ (f ∘ ⇑(LinearIsometryEquiv.symm v.repr)) (v.repr ξ)
Tactic:
rw [fourierIntegral_eq_fourierIntegral_euclidean_ofOrthonormalBasis v]
Proof state after:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝⁸ : Fintype ι
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : MeasurableSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : CompleteSpace F
v : OrthonormalBasis ι ℝ E
f : E → F
ξ : E
⊢ 𝓕ᵥ (f ∘ ⇑(LinearIsometryEquiv.symm v.repr)) (v.repr ξ) = 𝓕ₙ (f ∘ ⇑(LinearIsometryEquiv.symm v.repr)) (v.repr ξ)
Theorem: RealVectorFourier.fourierIntegral_eq_fourierIntegral_l2inner_ofOrthonormalBasis
Proof state before:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝⁸ : Fintype ι
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : MeasurableSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : CompleteSpace F
v : OrthonormalBasis ι ℝ E
f : E → F
ξ : E
⊢ 𝓕ᵥ (f ∘ ⇑(LinearIsometryEquiv.symm v.repr)) (v.repr ξ) = 𝓕ₙ (f ∘ ⇑(LinearIsometryEquiv.symm v.repr)) (v.repr ξ)
Tactic:
rw [fourierIntegral_euclidean_eq_fourierIntegral_l2inner]
Proof state after:
no goals