awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Fourier.RiemannLebesgueLemma (goal)
Goal:
E : Type u_1
V : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : V → E
inst_2 : NormedAddCommGroup V
inst_3 : MeasurableSpace V
inst_4 : BorelSpace V
inst_5 : InnerProductSpace ℝ V
inst_6 : FiniteDimensional ℝ V
μ : Measure V
inst_7 : μ.IsAddHaarMeasure
⊢ Tendsto.{u_2, u_1} (β := E)
    (fun (w : StrongDual ℝ V) ↦
      ∫ (v : V), HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-(w : (a : V) → ℝ) v) : Circle) (f v) ∂μ)
    (cocompact (StrongDual ℝ V)) (𝓝 0)
have rw : Tendsto.{u_2, u_1} (β := E)
  (fun (w : StrongDual ℝ V) ↦
    ∫ (v : V),
      HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-(w : (a : V) → ℝ) v) : Circle)
        (f v) ∂HSMul.hSMul (β := Measure V) (μ.addHaarScalarFactor volume) (volume : Measure V))
  (cocompact (StrongDual ℝ V)) (𝓝 0)
Tactic: rw [μ.isAddLeftInvariant_eq_smul volume]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.RiemannLebesgueLemma (goal)
Goal:
E : Type u_1
V : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : V → E
inst_2 : NormedAddCommGroup V
inst_3 : MeasurableSpace V
inst_4 : BorelSpace V
inst_5 : InnerProductSpace ℝ V
inst_6 : FiniteDimensional ℝ V
μ : Measure V
inst_7 : μ.IsAddHaarMeasure
⊢ Tendsto.{u_2, u_1} (β := E)
    (fun (w : StrongDual ℝ V) ↦
      ∫ (v : V),
        HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-(w : (a : V) → ℝ) v) : Circle)
          (f v) ∂HSMul.hSMul (β := Measure V) (μ.addHaarScalarFactor volume) (volume : Measure V))
    (cocompact (StrongDual ℝ V)) (𝓝 0)
have simp_rw : Tendsto.{u_2, u_1} (β := E)
  (fun (w : StrongDual ℝ V) ↦
    HSMul.hSMul (β := E) (μ.addHaarScalarFactor volume)
      (@integral _ _ _ _ inst_3 (volume : Measure V) fun (v : V) ↦
        HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-(w : (a : V) → ℝ) v) : Circle) (f v)))
  (cocompact (StrongDual ℝ V)) (𝓝 0)
Tactic: simp_rw [integral_smul_nnreal_measure]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.RiemannLebesgueLemma (goal)
Goal:
E : Type u_1
V : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : V → E
inst_2 : NormedAddCommGroup V
inst_3 : MeasurableSpace V
inst_4 : BorelSpace V
inst_5 : InnerProductSpace ℝ V
inst_6 : FiniteDimensional ℝ V
μ : Measure V
inst_7 : μ.IsAddHaarMeasure
⊢ Tendsto.{u_2, u_1} (β := E)
    (fun (w : StrongDual ℝ V) ↦
      HSMul.hSMul (β := E) (μ.addHaarScalarFactor volume)
        (@integral _ _ _ _ inst_3 (volume : Measure V) fun (v : V) ↦
          HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-(w : (a : V) → ℝ) v) : Circle) (f v)))
    (cocompact (StrongDual ℝ V)) (𝓝 0)
have rw : Tendsto
  (fun (w : StrongDual ℝ V) ↦
    HSMul.hSMul (β := E) (μ.addHaarScalarFactor volume)
      (@integral _ _ _ _ inst_3 (volume : Measure V) fun (v : V) ↦
        HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-(w : (a : V) → ℝ) v) : Circle) (f v)))
  (cocompact (StrongDual ℝ V)) (𝓝 (HSMul.hSMul (β := E) (μ.addHaarScalarFactor volume) 0))
Tactic: rw [← (smul_zero _ : Measure.addHaarScalarFactor μ volume • (0 : E) = 0)]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.RiemannLebesgueLemma (goal)
Goal:
E : Type u_1
V : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : V → E
inst_2 : NormedAddCommGroup V
inst_3 : MeasurableSpace V
inst_4 : BorelSpace V
inst_5 : InnerProductSpace ℝ V
inst_6 : FiniteDimensional ℝ V
μ : Measure V
inst_7 : μ.IsAddHaarMeasure
⊢ Tendsto
    (fun (w : StrongDual ℝ V) ↦
      HSMul.hSMul (β := E) (μ.addHaarScalarFactor volume)
        (@integral _ _ _ _ inst_3 (volume : Measure V) fun (v : V) ↦
          HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-(w : (a : V) → ℝ) v) : Circle) (f v)))
    (cocompact (StrongDual ℝ V)) (𝓝 (HSMul.hSMul (β := E) (μ.addHaarScalarFactor volume) 0))
have hf : Tendsto.{u_2, u_1} (β := E)
  (fun (x : StrongDual ℝ V) ↦
    @integral _ _ _ _ inst_3 (volume : Measure V) fun (v : V) ↦
      HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-(x : (a : V) → ℝ) v) : Circle) (f v))
  (cocompact (StrongDual ℝ V)) (𝓝 0)
Tactic: apply Tendsto.const_smul
-- Lean 4 proof step from Mathlib.Analysis.Fourier.RiemannLebesgueLemma (goal)
Goal:
E : Type u_1
V : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : V → E
inst_2 : NormedAddCommGroup V
inst_3 : MeasurableSpace V
inst_4 : BorelSpace V
inst_5 : InnerProductSpace ℝ V
inst_6 : FiniteDimensional ℝ V
μ : Measure V
inst_7 : μ.IsAddHaarMeasure
A : StrongDual ℝ V ≃ₗᵢ⋆[ℝ] V := LinearIsometryEquiv.symm (InnerProductSpace.toDual ℝ V)
⊢ Eq (α := (w : StrongDual ℝ V) → E)
    (fun (w : StrongDual ℝ V) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
        HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-(w : (a : V) → ℝ) v) : Circle) (f v))
    ((fun (w : V) ↦
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
          HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f v)) ∘
      (⇑A : (a : StrongDual ℝ V) → V))
have h : ∀ (w : StrongDual ℝ V),
  Eq.{u_1 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
      HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-(w : (a : V) → ℝ) v) : Circle) (f v))
    (((fun (w : V) ↦
          @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
            HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f v)) ∘
        (⇑A : (a : StrongDual ℝ V) → V))
      w)
Tactic: ext1 w
-- Lean 4 proof step from Mathlib.Analysis.Fourier.RiemannLebesgueLemma (goal)
Goal:
E : Type u_1
V : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : V → E
inst_2 : NormedAddCommGroup V
inst_3 : MeasurableSpace V
inst_4 : BorelSpace V
inst_5 : InnerProductSpace ℝ V
inst_6 : FiniteDimensional ℝ V
μ : Measure V
inst_7 : μ.IsAddHaarMeasure
A : StrongDual ℝ V ≃ₗᵢ⋆[ℝ] V := LinearIsometryEquiv.symm (InnerProductSpace.toDual ℝ V)
w : StrongDual ℝ V
⊢ Eq.{u_1 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
      HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-(w : (a : V) → ℝ) v) : Circle) (f v))
    (((fun (w : V) ↦
          @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
            HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f v)) ∘
        (⇑A : (a : StrongDual ℝ V) → V))
      w)
have h : ∀ (v : V),
  HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-(w : (a : V) → ℝ) v) : Circle) (f v) =
    HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, (A : (a : StrongDual ℝ V) → V) w⟫) : Circle) (f v)
Tactic: congr 1 with v : 1
-- Lean 4 proof step from Mathlib.Analysis.Fourier.RiemannLebesgueLemma (goal)
Goal:
E : Type u_1
V : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : V → E
inst_2 : NormedAddCommGroup V
inst_3 : MeasurableSpace V
inst_4 : BorelSpace V
inst_5 : InnerProductSpace ℝ V
inst_6 : FiniteDimensional ℝ V
μ : Measure V
inst_7 : μ.IsAddHaarMeasure
A : StrongDual ℝ V ≃ₗᵢ⋆[ℝ] V := LinearIsometryEquiv.symm (InnerProductSpace.toDual ℝ V)
w : StrongDual ℝ V
v : V
⊢ HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-(w : (a : V) → ℝ) v) : Circle) (f v) =
    HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, (A : (a : StrongDual ℝ V) → V) w⟫) : Circle) (f v)
have h : HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-(w : (a : V) → ℝ) v) : Circle) (f v) =
  HSMul.hSMul (α := Circle)
    ((𝐞 : (a : ℝ) → Circle) (-(starRingEnd ℝ : (a : ℝ) → ℝ) ⟪(A : (a : StrongDual ℝ V) → V) w, v⟫) : Circle) (f v)
Tactic: rw [← inner_conj_symm, RCLike.conj_to_real, InnerProductSpace.toDual_symm_apply]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.RiemannLebesgueLemma (goal)
Goal:
E : Type u_1
V : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : V → E
inst_2 : NormedAddCommGroup V
inst_3 : MeasurableSpace V
inst_4 : BorelSpace V
inst_5 : InnerProductSpace ℝ V
inst_6 : FiniteDimensional ℝ V
μ : Measure V
inst_7 : μ.IsAddHaarMeasure
A : StrongDual ℝ V ≃ₗᵢ⋆[ℝ] V := LinearIsometryEquiv.symm (InnerProductSpace.toDual ℝ V)
w : StrongDual ℝ V
v : V
h :
  HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-(w : (a : V) → ℝ) v) : Circle) (f v) =
    HSMul.hSMul (α := Circle)
      ((𝐞 : (a : ℝ) → Circle) (-(starRingEnd ℝ : (a : ℝ) → ℝ) ⟪(A : (a : StrongDual ℝ V) → V) w, v⟫) : Circle) (f v)
⊢ HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-(w : (a : V) → ℝ) v) : Circle) (f v) =
    HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, (A : (a : StrongDual ℝ V) → V) w⟫) : Circle) (f v)
have h₁ : HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-(w : (a : V) → ℝ) v) : Circle) (f v) =
  HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪(A : (a : StrongDual ℝ V) → V) w, v⟫) : Circle) (f v)
Tactic: rw [← inner_conj_symm, RCLike.conj_to_real, InnerProductSpace.toDual_symm_apply]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.RiemannLebesgueLemma (goal)
Goal:
E : Type u_1
V : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : V → E
inst_2 : NormedAddCommGroup V
inst_3 : MeasurableSpace V
inst_4 : BorelSpace V
inst_5 : InnerProductSpace ℝ V
inst_6 : FiniteDimensional ℝ V
μ : Measure V
inst_7 : μ.IsAddHaarMeasure
A : StrongDual ℝ V ≃ₗᵢ⋆[ℝ] V := LinearIsometryEquiv.symm (InnerProductSpace.toDual ℝ V)
w : StrongDual ℝ V
v : V
h :
  HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-(w : (a : V) → ℝ) v) : Circle) (f v) =
    HSMul.hSMul (α := Circle)
      ((𝐞 : (a : ℝ) → Circle) (-(starRingEnd ℝ : (a : ℝ) → ℝ) ⟪(A : (a : StrongDual ℝ V) → V) w, v⟫) : Circle) (f v)
h₁ :
  HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-(w : (a : V) → ℝ) v) : Circle) (f v) =
    HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪(A : (a : StrongDual ℝ V) → V) w, v⟫) : Circle) (f v)
⊢ HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-(w : (a : V) → ℝ) v) : Circle) (f v) =
    HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, (A : (a : StrongDual ℝ V) → V) w⟫) : Circle) (f v)
have h₂ : HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-(w : (a : V) → ℝ) v) : Circle) (f v) =
  HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-(w : (a : V) → ℝ) v) : Circle) (f v)
Tactic: rw [← inner_conj_symm, RCLike.conj_to_real, InnerProductSpace.toDual_symm_apply]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.RiemannLebesgueLemma (hypothesis)
Goal:
E : Type u_1
V : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : V → E
inst_2 : NormedAddCommGroup V
inst_3 : MeasurableSpace V
inst_4 : BorelSpace V
inst_5 : InnerProductSpace ℝ V
inst_6 : FiniteDimensional ℝ V
μ : Measure V
inst_7 : μ.IsAddHaarMeasure
A : StrongDual ℝ V ≃ₗᵢ⋆[ℝ] V := LinearIsometryEquiv.symm (InnerProductSpace.toDual ℝ V)
⊢ Tendsto.{u_2, u_1} (β := E)
    (fun (x : StrongDual ℝ V) ↦
      @integral _ _ _ _ inst_3 (volume : Measure V) fun (v : V) ↦
        HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-(x : (a : V) → ℝ) v) : Circle) (f v))
    (cocompact (StrongDual ℝ V)) (𝓝 0)
have this : Eq (α := (w : StrongDual ℝ V) → E)
  (fun (w : StrongDual ℝ V) ↦
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
      HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-(w : (a : V) → ℝ) v) : Circle) (f v))
  ((fun (w : V) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
        HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f v)) ∘
    (⇑A : (a : StrongDual ℝ V) → V))
Tactic: have : (fun w : StrongDual ℝ V ↦ ∫ v, 𝐞 (-w v) • f v) =
      (fun w : V ↦ ∫ v, 𝐞 (-⟪v, w⟫) • f v) ∘ A := by
    ext1 w
    congr 1 with v : 1
    rw [← inner_conj_symm, RCLike.conj_to_real, InnerProductSpace.toDual_symm_apply]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.RiemannLebesgueLemma (goal)
Goal:
E : Type u_1
V : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : V → E
inst_2 : NormedAddCommGroup V
inst_3 : MeasurableSpace V
inst_4 : BorelSpace V
inst_5 : InnerProductSpace ℝ V
inst_6 : FiniteDimensional ℝ V
μ : Measure V
inst_7 : μ.IsAddHaarMeasure
A : StrongDual ℝ V ≃ₗᵢ⋆[ℝ] V := LinearIsometryEquiv.symm (InnerProductSpace.toDual ℝ V)
this :
  Eq (α := (w : StrongDual ℝ V) → E)
    (fun (w : StrongDual ℝ V) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
        HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-(w : (a : V) → ℝ) v) : Circle) (f v))
    ((fun (w : V) ↦
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
          HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f v)) ∘
      (⇑A : (a : StrongDual ℝ V) → V))
⊢ Tendsto.{u_2, u_1} (β := E)
    (fun (x : StrongDual ℝ V) ↦
      @integral _ _ _ _ inst_3 (volume : Measure V) fun (v : V) ↦
        HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-(x : (a : V) → ℝ) v) : Circle) (f v))
    (cocompact (StrongDual ℝ V)) (𝓝 0)
have hf : Tendsto.{u_2, u_1} (α := StrongDual ℝ V) (β := E)
  ((fun (w : V) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
        HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f v)) ∘
    (⇑A : (a : StrongDual ℝ V) → V))
  (cocompact (StrongDual ℝ V)) (𝓝 0)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.RiemannLebesgueLemma (goal)
Goal:
E : Type u_1
V : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : V → E
inst_2 : AddCommGroup V
inst_3 : TopologicalSpace V
inst_4 : IsTopologicalAddGroup V
inst_5 : T2Space V
inst_6 : MeasurableSpace V
inst_7 : BorelSpace V
inst_8 : Module ℝ V
inst_9 : ContinuousSMul ℝ V
inst_10 : FiniteDimensional ℝ V
μ : Measure V
inst_11 : μ.IsAddHaarMeasure
V' : Type := EuclideanSpace ℝ (Fin (finrank ℝ V))
⊢ Tendsto.{u_2, u_1} (β := E)
    (fun (w : StrongDual ℝ V) ↦
      ∫ (v : V), HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-(w : (a : V) → ℝ) v) : Circle) (f v) ∂μ)
    (cocompact (StrongDual ℝ V)) (𝓝 0)
have have : ∀ (A : V ≃L[ℝ] V'),
  Tendsto.{u_2, u_1} (β := E)
    (fun (w : StrongDual ℝ V) ↦
      ∫ (v : V), HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-(w : (a : V) → ℝ) v) : Circle) (f v) ∂μ)
    (cocompact (StrongDual ℝ V)) (𝓝 0)
Tactic: have A : V ≃L[ℝ] V' := toEuclidean
-- Lean 4 proof step from Mathlib.Analysis.Fourier.RiemannLebesgueLemma (hypothesis)
Goal:
E : Type u_1
V : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : V → E
inst_2 : AddCommGroup V
inst_3 : TopologicalSpace V
inst_4 : IsTopologicalAddGroup V
inst_5 : T2Space V
inst_6 : MeasurableSpace V
inst_7 : BorelSpace V
inst_8 : Module ℝ V
inst_9 : ContinuousSMul ℝ V
inst_10 : FiniteDimensional ℝ V
μ : Measure V
inst_11 : μ.IsAddHaarMeasure
V' : Type := EuclideanSpace ℝ (Fin (finrank ℝ V))
A : V ≃L[ℝ] V'
⊢ Tendsto.{u_2, u_1} (β := E)
    (fun (w : StrongDual ℝ V) ↦
      ∫ (v : V), HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-(w : (a : V) → ℝ) v) : Circle) (f v) ∂μ)
    (cocompact (StrongDual ℝ V)) (𝓝 0)
have this : let this := borel V';
BorelSpace V'
Tactic: borelize V'
-- Lean 4 proof step from Mathlib.Analysis.Fourier.RiemannLebesgueLemma (hypothesis)
Goal:
E : Type u_1
V : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : V → E
inst_2 : AddCommGroup V
inst_3 : TopologicalSpace V
inst_4 : IsTopologicalAddGroup V
inst_5 : T2Space V
inst_6 : MeasurableSpace V
inst_7 : BorelSpace V
inst_8 : Module ℝ V
inst_9 : ContinuousSMul ℝ V
inst_10 : FiniteDimensional ℝ V
μ : Measure V
inst_11 : μ.IsAddHaarMeasure
V' : Type := EuclideanSpace ℝ (Fin (finrank ℝ V))
A : V ≃L[ℝ] V'
this : MeasurableSpace V' := borel V'
this_1 : BorelSpace V'
Aₘ : V ≃ᵐ V' := A.toHomeomorph.toMeasurableEquiv
Adual : StrongDual ℝ V ≃L[ℝ] StrongDual ℝ V' := A.arrowCongrSL (ContinuousLinearEquiv.refl ℝ ℝ)
⊢ Tendsto.{u_2, u_1} (β := E)
    (fun (w : StrongDual ℝ V) ↦
      ∫ (v : V), HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-(w : (a : V) → ℝ) v) : Circle) (f v) ∂μ)
    (cocompact (StrongDual ℝ V)) (𝓝 0)
have this : Measure.IsAddHaarMeasure (G := V') (Measure.map (⇑Aₘ : (a : V) → V') μ)
Tactic: have : (μ.map Aₘ).IsAddHaarMeasure := A.isAddHaarMeasure_map _
-- Lean 4 proof step from Mathlib.Analysis.Fourier.RiemannLebesgueLemma (goal)
Goal:
E : Type u_1
V : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : V → E
inst_2 : AddCommGroup V
inst_3 : TopologicalSpace V
inst_4 : IsTopologicalAddGroup V
inst_5 : T2Space V
inst_6 : MeasurableSpace V
inst_7 : BorelSpace V
inst_8 : Module ℝ V
inst_9 : ContinuousSMul ℝ V
inst_10 : FiniteDimensional ℝ V
μ : Measure V
inst_11 : μ.IsAddHaarMeasure
V' : Type := EuclideanSpace ℝ (Fin (finrank ℝ V))
A : V ≃L[ℝ] V'
this_1 : MeasurableSpace V' := borel V'
this_2 : BorelSpace V'
Aₘ : V ≃ᵐ V' := A.toHomeomorph.toMeasurableEquiv
Adual : StrongDual ℝ V ≃L[ℝ] StrongDual ℝ V' := A.arrowCongrSL (ContinuousLinearEquiv.refl ℝ ℝ)
this : Measure.IsAddHaarMeasure (G := V') (Measure.map (⇑Aₘ : (a : V) → V') μ)
⊢ Tendsto.{u_2, u_1} (β := E)
    (fun (w : StrongDual ℝ V) ↦
      ∫ (v : V), HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-(w : (a : V) → ℝ) v) : Circle) (f v) ∂μ)
    (cocompact (StrongDual ℝ V)) (𝓝 0)
have h : ∀ (w : StrongDual ℝ V),
  Eq.{u_1 + 1} (α := E)
    (∫ (v : V), HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-(w : (a : V) → ℝ) v) : Circle) (f v) ∂μ)
    (((fun (w : StrongDual ℝ V') ↦
          @integral _ _ _ _ this_1 (Measure.map (⇑Aₘ : (a : V) → V') μ) fun (v : V') ↦
            HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-(w : (a : V') → ℝ) v) : Circle)
              ((f ∘ (⇑A.symm : (a : V') → V)) v)) ∘
        Adual.toHomeomorph.toCocompactMap.toFun)
      w)
Tactic: convert!
    (tendsto_integral_exp_smul_cocompact_of_inner_product (f ∘ A.symm) (μ.map Aₘ)).comp
      Adual.toHomeomorph.toCocompactMap.cocompact_tendsto' with
    w
-- Lean 4 proof step from Mathlib.Analysis.Fourier.RiemannLebesgueLemma (goal)
Goal:
E : Type u_1
V : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : V → E
inst_2 : AddCommGroup V
inst_3 : TopologicalSpace V
inst_4 : IsTopologicalAddGroup V
inst_5 : T2Space V
inst_6 : MeasurableSpace V
inst_7 : BorelSpace V
inst_8 : Module ℝ V
inst_9 : ContinuousSMul ℝ V
inst_10 : FiniteDimensional ℝ V
μ : Measure V
inst_11 : μ.IsAddHaarMeasure
V' : Type := EuclideanSpace ℝ (Fin (finrank ℝ V))
A : V ≃L[ℝ] V'
this_1 : MeasurableSpace V' := borel V'
this_2 : BorelSpace V'
Aₘ : V ≃ᵐ V' := A.toHomeomorph.toMeasurableEquiv
Adual : StrongDual ℝ V ≃L[ℝ] StrongDual ℝ V' := A.arrowCongrSL (ContinuousLinearEquiv.refl ℝ ℝ)
this : Measure.IsAddHaarMeasure (G := V') (Measure.map (⇑Aₘ : (a : V) → V') μ)
w : StrongDual ℝ V
⊢ Eq.{u_1 + 1} (α := E)
    (∫ (v : V), HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-(w : (a : V) → ℝ) v) : Circle) (f v) ∂μ)
    (((fun (w : StrongDual ℝ V') ↦
          @integral _ _ _ _ this_1 (Measure.map (⇑Aₘ : (a : V) → V') μ) fun (v : V') ↦
            HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-(w : (a : V') → ℝ) v) : Circle)
              ((f ∘ (⇑A.symm : (a : V') → V)) v)) ∘
        Adual.toHomeomorph.toCocompactMap.toFun)
      w)
have h : Eq.{u_1 + 1} (α := E)
  (∫ (v : V), HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-(w : (a : V) → ℝ) v) : Circle) (f v) ∂μ)
  (∫ (x : V),
    HSMul.hSMul (α := Circle)
      ((𝐞 : (a : ℝ) → Circle) (-(w : (a : V) → ℝ) ((A.symm : (a : V') → V) ((Aₘ : (a : V) → V') x : V') : V)) : Circle)
      (f ((A.symm : (a : V') → V) ((Aₘ : (a : V) → V') x : V'))) ∂μ)
Tactic: suffices ∫ v, 𝐞 (-w v) • f v ∂μ = ∫ (x : V), 𝐞 (-w (A.symm (Aₘ x))) • f (A.symm (Aₘ x)) ∂μ by
    simpa [Function.comp_apply, integral_map_equiv, Adual]
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
ι : Type u_1
A : ι → Type u_2
inst : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst_1 : DecidableEq ι
p : ℝ
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
s : Finset ι
hp : (↑(#s) : ℝ) * p ≤ 1
i : ι
hi : i ∉ s
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
⊢ T (A := A) μ p f (insert i s) =
    lmarginal (X := A) μ (insert i s) (f ^ (1 - (↑(#s) : ℝ) * p) * ∏ j ∈ insert i s, lmarginal (X := A) μ {j} f ^ p)
have simp_rw : lmarginal (X := A) μ (insert i s)
    (f ^ (1 - HSub.hSub (α := ℝ) (↑(#s + 1) : ℝ) 1 * p) * ∏ i ∈ insert i s, lmarginal (X := A) μ {i} f ^ p) =
  lmarginal (X := A) μ (insert i s) (f ^ (1 - (↑(#s) : ℝ) * p) * ∏ i ∈ insert i s, lmarginal (X := A) μ {i} f ^ p)
Tactic: simp_rw [T, card_insert_of_notMem hi]
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
ι : Type u_1
A : ι → Type u_2
inst : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst_1 : DecidableEq ι
p : ℝ
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
s : Finset ι
hp : (↑(#s) : ℝ) * p ≤ 1
i : ι
hi : i ∉ s
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
⊢ lmarginal (X := A) μ (insert i s)
      (f ^ (1 - HSub.hSub (α := ℝ) (↑(#s + 1) : ℝ) 1 * p) * ∏ i ∈ insert i s, lmarginal (X := A) μ {i} f ^ p) =
    lmarginal (X := A) μ (insert i s) (f ^ (1 - (↑(#s) : ℝ) * p) * ∏ i ∈ insert i s, lmarginal (X := A) μ {i} f ^ p)
have h : HSub.hSub (α := ℝ) (↑(#s + 1) : ℝ) 1 = (↑(#s) : ℝ)
Tactic: congr!
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
ι : Type u_1
A : ι → Type u_2
inst : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst_1 : DecidableEq ι
p : ℝ
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
s : Finset ι
hp : (↑(#s) : ℝ) * p ≤ 1
i : ι
hi : i ∉ s
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
⊢ HSub.hSub (α := ℝ) (↑(#s + 1) : ℝ) 1 = (↑(#s) : ℝ)
have h : HAdd.hAdd (α := ℝ) (↑(#s) : ℝ) 1 - 1 = (↑(#s) : ℝ)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
ι : Type u_1
A : ι → Type u_2
inst : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst_1 : DecidableEq ι
p : ℝ
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
s : Finset ι
hp : (↑(#s) : ℝ) * p ≤ 1
i : ι
hi : i ∉ s
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
⊢ lmarginal (X := A) μ (insert i s) (f ^ (1 - (↑(#s) : ℝ) * p) * ∏ j ∈ insert i s, lmarginal (X := A) μ {j} f ^ p) =
    lmarginal (X := A) μ s fun (x : (i : ι) → A i) ↦
      ∫⁻ (t : A i),
        f (update (β := A) x i t) ^ (1 - (↑(#s) : ℝ) * p) *
          ∏ j ∈ insert i s, lmarginal (X := A) μ {j} f (update (β := A) x i t) ^ p ∂μ i
have rw : (lmarginal (X := A) μ s fun (x : (i : ι) → A i) ↦
    ∫⁻ (xᵢ : A i),
      HMul.hMul (β := (x : (i : ι) → A i) → ℝ≥0∞) (f ^ (1 - (↑(#s) : ℝ) * p))
        (∏ j ∈ insert i s, lmarginal (X := A) μ {j} f ^ p) (update (β := A) x i xᵢ) ∂μ i) =
  lmarginal (X := A) μ s fun (x : (i : ι) → A i) ↦
    ∫⁻ (t : A i),
      f (update (β := A) x i t) ^ (1 - (↑(#s) : ℝ) * p) *
        ∏ j ∈ insert i s, lmarginal (X := A) μ {j} f (update (β := A) x i t) ^ p ∂μ i
Tactic: rw [lmarginal_insert' _ _ hi]
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
ι : Type u_1
A : ι → Type u_2
inst : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst_1 : DecidableEq ι
p : ℝ
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
s : Finset ι
hp : (↑(#s) : ℝ) * p ≤ 1
i : ι
hi : i ∉ s
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
rw :
  (lmarginal (X := A) μ s fun (x : (i : ι) → A i) ↦
      ∫⁻ (xᵢ : A i),
        HMul.hMul (β := (x : (i : ι) → A i) → ℝ≥0∞) (f ^ (1 - (↑(#s) : ℝ) * p))
          (∏ j ∈ insert i s, lmarginal (X := A) μ {j} f ^ p) (update (β := A) x i xᵢ) ∂μ i) =
    lmarginal (X := A) μ s fun (x : (i : ι) → A i) ↦
      ∫⁻ (t : A i),
        f (update (β := A) x i t) ^ (1 - (↑(#s) : ℝ) * p) *
          ∏ j ∈ insert i s, lmarginal (X := A) μ {j} f (update (β := A) x i t) ^ p ∂μ i
⊢ lmarginal (X := A) μ (insert i s) (f ^ (1 - (↑(#s) : ℝ) * p) * ∏ j ∈ insert i s, lmarginal (X := A) μ {j} f ^ p) =
    lmarginal (X := A) μ s fun (x : (i : ι) → A i) ↦
      ∫⁻ (t : A i),
        f (update (β := A) x i t) ^ (1 - (↑(#s) : ℝ) * p) *
          ∏ j ∈ insert i s, lmarginal (X := A) μ {j} f (update (β := A) x i t) ^ p ∂μ i
have rw₁ : Measurable (f ^ (1 - (↑(#s) : ℝ) * p) * ∏ j ∈ insert i s, lmarginal (X := A) μ {j} f ^ p)
Tactic: rw [lmarginal_insert' _ _ hi]