awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
p : ℝ≥0
hp : (↑p : ℝ≥0∞) ≠ 0
h_one_add : ∀ (x : E), 0 < 1 + ‖x‖
hp_pos : 0 < (↑p : ℝ)
l : ℕ
hl : Integrable (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑l : ℝ))) μ
k : ℕ := ⌈(↑l : ℝ) / (↑p : ℝ)⌉₊
hlk : (↑l : ℝ) ≤ (↑k : ℝ) * (↑p : ℝ)
x : E
⊢ 1 ≤ 1 + ‖x‖

Tactic:
simp
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
p : ℝ≥0
⊢ (↑p : ℝ≥0∞) = 0 ∨ (↑p : ℝ≥0∞) ≠ 0

Tactic:
cases eq_or_ne (p : ℝ≥0∞) 0 with
    | inl hp => exact ⟨0, by simp [hp]⟩
    | inr hp =>
      have h_one_add (x : E) : 0 < 1 + ‖x‖ := lt_add_of_pos_of_le zero_lt_one (norm_nonneg x)
      have hp_pos : 0 < (p : ℝ) := by simpa [zero_lt_iff] using hp
      rcases hμ.exists_integrable with ⟨l, hl⟩
      let k := ⌈(l / p : ℝ)⌉₊
      have hlk : l ≤ k * (p : ℝ) := by simpa [div_le_iff₀ hp_pos] using Nat.le_ceil (l / p : ℝ)
      use k
      suffices HasFiniteIntegral (fun x ↦ ((1 + ‖x‖) ^ (-(k * p) : ℝ))) μ by
        rw [hasFiniteIntegral_iff_enorm] at this
        rw [eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top hp ENNReal.coe_ne_top]
        simp only [ENNReal.coe_toReal]
        refine Eq.subst (motive := (∫⁻ x, · x ∂μ < ⊤)) (funext fun x ↦ ?_) this
        rw [← neg_mul, Real.rpow_mul (h_one_add x).le]
        exact Real.enorm_rpow_of_nonneg (by positivity) NNReal.zero_le_coe
      refine hl.hasFiniteIntegral.mono' (ae_of_all μ fun x ↦ ?_)
      rw [Real.norm_of_nonneg (Real.rpow_nonneg (h_one_add x).le _)]
      gcongr
      simp

Premises used: ENNReal.ofNNReal, MeasureTheory.Measure.HasTemperateGrowth.exists_integrable, eq_or_ne, OfNat.ofNat
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
p : ℝ≥0∞
μ : Measure E
hμ : μ.HasTemperateGrowth
top : ∃ (k : ℕ), eLpNorm (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ))) ∞ μ < ∞
coe :
  ∀ (p : ℝ≥0), ∃ (k : ℕ), eLpNorm (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ))) (↑p : ℝ≥0∞) μ < ∞
⊢ ∃ (k : ℕ), eLpNorm (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ))) p μ < ∞

Tactic:
cases p with
  | top => exact ⟨0, eLpNormEssSup_lt_top_of_ae_bound (C := 1) (by simp)⟩
  | coe p =>
    cases eq_or_ne (p : ℝ≥0∞) 0 with
    | inl hp => exact ⟨0, by simp [hp]⟩
    | inr hp =>
      have h_one_add (x : E) : 0 < 1 + ‖x‖ := lt_add_of_pos_of_le zero_lt_one (norm_nonneg x)
      have hp_pos : 0 < (p : ℝ) := by simpa [zero_lt_iff] using hp
      rcases hμ.exists_integrable with ⟨l, hl⟩
      let k := ⌈(l / p : ℝ)⌉₊
      have hlk : l ≤ k * (p : ℝ) := by simpa [div_le_iff₀ hp_pos] using Nat.le_ceil (l / p : ℝ)
      use k
      suffices HasFiniteIntegral (fun x ↦ ((1 + ‖x‖) ^ (-(k * p) : ℝ))) μ by
        rw [hasFiniteIntegral_iff_enorm] at this
        rw [eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top hp ENNReal.coe_ne_top]
        simp only [ENNReal.coe_toReal]
        refine Eq.subst (motive := (∫⁻ x, · x ∂μ < ⊤)) (funext fun x ↦ ?_) this
        rw [← neg_mul, Real.rpow_mul (h_one_add x).le]
        exact Real.enorm_rpow_of_nonneg (by positivity) NNReal.zero_le_coe
      refine hl.hasFiniteIntegral.mono' (ae_of_all μ fun x ↦ ?_)
      rw [Real.norm_of_nonneg (Real.rpow_nonneg (h_one_add x).le _)]
      gcongr
      simp

Premises used: MeasureTheory.Measure.HasTemperateGrowth.exists_integrable, eq_or_ne, OfNat.ofNat
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
μ : Measure E
hμ : μ.HasTemperateGrowth
g : 𝓢(E, ℂ)
⊢ Eq (α := ℂ) ((μ.toTemperedDistribution : (a : 𝓢(E, ℂ)) → ℂ) g : ℂ) (∫ (x : E), (g : (a : E) → ℂ) x ∂μ : ℂ)

Tactic:
rfl
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : SecondCountableTopology E
μ : Measure E
hμ : μ.HasTemperateGrowth
f : E → F
hf : HasTemperateGrowth f
g : 𝓢(E, ℂ)
⊢ Eq.{u_4 + 1} (α := F) ((toTemperedDistribution μ hf : (a : 𝓢(E, ℂ)) → F) g : F)
    (∫ (x : E), HSMul.hSMul (α := ℂ) ((g : (a : E) → ℂ) x : ℂ) (f x) ∂μ : F)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
F₁ : Type u_5
F₂ : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : SecondCountableTopology E
μ : Measure E
hμ : μ.HasTemperateGrowth
x x_1 : 𝓢(E, F)
⊢ (toPointwiseConvergenceCLM ℂ (RingHom.id ℂ) 𝓢(E, ℂ) F : (a : 𝓢(E, ℂ) →L[ℂ] F) → 𝓢(E, ℂ) →Lₚₜ[ℂ] F)
      (comp (σ₁₂ := RingHom.id ℂ) (M₂ := 𝓢(E, F)) (integralCLM ℂ μ)
        (((pairing (ContinuousLinearMap.flip (lsmul ℂ ℂ)) : 𝓢(E, F) →ₗ[ℂ] 𝓢(E, ℂ) →L[ℂ] 𝓢(E, F)) :
            (a : 𝓢(E, F)) → 𝓢(E, ℂ) →L[ℂ] 𝓢(E, F))
          (x + x_1))) =
    HAdd.hAdd (α := 𝓢'(E, F)) (β := 𝓢'(E, F))
      ((toPointwiseConvergenceCLM ℂ (RingHom.id ℂ) 𝓢(E, ℂ) F : (a : 𝓢(E, ℂ) →L[ℂ] F) → 𝓢(E, ℂ) →Lₚₜ[ℂ] F)
          (comp (σ₁₂ := RingHom.id ℂ) (M₂ := 𝓢(E, F)) (integralCLM ℂ μ)
            (((pairing (ContinuousLinearMap.flip (lsmul ℂ ℂ)) : 𝓢(E, F) →ₗ[ℂ] 𝓢(E, ℂ) →L[ℂ] 𝓢(E, F)) :
                (a : 𝓢(E, F)) → 𝓢(E, ℂ) →L[ℂ] 𝓢(E, F))
              x)) :
        PointwiseConvergenceCLM.{0, 0, u_3, u_4} (RingHom.id ℂ) 𝓢(E, ℂ) F)
      ((toPointwiseConvergenceCLM ℂ (RingHom.id ℂ) 𝓢(E, ℂ) F : (a : 𝓢(E, ℂ) →L[ℂ] F) → 𝓢(E, ℂ) →Lₚₜ[ℂ] F)
          (comp (σ₁₂ := RingHom.id ℂ) (M₂ := 𝓢(E, F)) (integralCLM ℂ μ)
            (((pairing (ContinuousLinearMap.flip (lsmul ℂ ℂ)) : 𝓢(E, F) →ₗ[ℂ] 𝓢(E, ℂ) →L[ℂ] 𝓢(E, F)) :
                (a : 𝓢(E, F)) → 𝓢(E, ℂ) →L[ℂ] 𝓢(E, F))
              x_1)) :
        PointwiseConvergenceCLM.{0, 0, u_3, u_4} (RingHom.id ℂ) 𝓢(E, ℂ) F)

Tactic:
simp
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
F₁ : Type u_5
F₂ : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : SecondCountableTopology E
μ : Measure E
hμ : μ.HasTemperateGrowth
x : ℂ
x_1 : 𝓢(E, F)
⊢ (toPointwiseConvergenceCLM ℂ (RingHom.id ℂ) 𝓢(E, ℂ) F : (a : 𝓢(E, ℂ) →L[ℂ] F) → 𝓢(E, ℂ) →Lₚₜ[ℂ] F)
      (comp (σ₁₂ := RingHom.id ℂ) (M₂ := 𝓢(E, F)) (integralCLM ℂ μ)
        (((pairing (ContinuousLinearMap.flip (lsmul ℂ ℂ)) : 𝓢(E, F) →ₗ[ℂ] 𝓢(E, ℂ) →L[ℂ] 𝓢(E, F)) :
            (a : 𝓢(E, F)) → 𝓢(E, ℂ) →L[ℂ] 𝓢(E, F))
          (x • x_1))) =
    HSMul.hSMul (α := ℂ) (β := 𝓢'(E, F)) ((RingHom.id ℂ : (a : ℂ) → ℂ) x : ℂ)
      ((toPointwiseConvergenceCLM ℂ (RingHom.id ℂ) 𝓢(E, ℂ) F : (a : 𝓢(E, ℂ) →L[ℂ] F) → 𝓢(E, ℂ) →Lₚₜ[ℂ] F)
          (comp (σ₁₂ := RingHom.id ℂ) (M₂ := 𝓢(E, F)) (integralCLM ℂ μ)
            (((pairing (ContinuousLinearMap.flip (lsmul ℂ ℂ)) : 𝓢(E, F) →ₗ[ℂ] 𝓢(E, ℂ) →L[ℂ] 𝓢(E, F)) :
                (a : 𝓢(E, F)) → 𝓢(E, ℂ) →L[ℂ] 𝓢(E, F))
              x_1)) :
        PointwiseConvergenceCLM.{0, 0, u_3, u_4} (RingHom.id ℂ) 𝓢(E, ℂ) F)

Tactic:
simp
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : SecondCountableTopology E
μ : Measure E
hμ : μ.HasTemperateGrowth
f : 𝓢(E, F)
g : 𝓢(E, ℂ)
⊢ Eq.{u_4 + 1} (α := F)
    ((((toTemperedDistributionCLM E F μ : (a : 𝓢(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F)) : (a : 𝓢(E, ℂ)) → F) g : F)
    (∫ (x : E), HSMul.hSMul (α := ℂ) (β := F) ((g : (a : E) → ℂ) x : ℂ) ((f : (a : E) → F) x : F) ∂μ : F)

Tactic:
simp [toTemperedDistributionCLM, comp_apply _]

Premises used: ContinuousLinearMap.comp_apply
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : MeasureSpace E
inst_5 : BorelSpace E
inst_6 : SecondCountableTopology E
inst_7 : HasTemperateGrowth.{u_3} (E := E) volume
f : 𝓢(E, F)
g : 𝓢(E, ℂ)
⊢ Eq.{u_4 + 1} (α := F)
    ((((toTemperedDistributionCLM E F volume : (a : 𝓢(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F)) : (a : 𝓢(E, ℂ)) → F) g : F)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : E) ↦
        HSMul.hSMul (α := ℂ) (β := F) ((g : (a : E) → ℂ) x : ℂ) ((f : (a : E) → F) x : F) :
      F)

Tactic:
toTemperedDistributionCLM_apply_apply volume f g

Premises used: SchwartzMap.toTemperedDistributionCLM_apply_apply, MeasureTheory.MeasureSpace.volume
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
F₁ : Type u_5
F₂ : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : CompleteSpace F
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f : ↥(Lp F p μ)
this : p.HolderConjugate (1 - p⁻¹)⁻¹
⊢ Fact (1 ≤ (1 - p⁻¹)⁻¹)

Tactic:
simp [fact_iff]

Premises used: fact_iff
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : CompleteSpace F
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f : ↥(Lp F p μ)
g : 𝓢(E, ℂ)
simp :
  Eq.{u_4 + 1} (α := F)
    (∫ (x : E), (↑(↑(g.toLp (1 - p⁻¹)⁻¹ μ) : E →ₘ[μ] ℂ) : E → ℂ) x • (↑(↑f : E →ₘ[μ] F) : E → F) x ∂μ)
    (∫ (x : E), HSMul.hSMul (α := ℂ) ((g : (a : E) → ℂ) x : ℂ) ((↑(↑f : E →ₘ[μ] F) : E → F) x) ∂μ)
⊢ Eq.{u_4 + 1} (α := F) ((toTemperedDistribution f : (a : 𝓢(E, ℂ)) → F) g : F)
    (∫ (x : E), HSMul.hSMul (α := ℂ) ((g : (a : E) → ℂ) x : ℂ) ((↑(↑f : E →ₘ[μ] F) : E → F) x) ∂μ : F)

Tactic:
simp only [toTemperedDistribution, toPointwiseConvergenceCLM_apply, comp_apply _, toLpCLM_apply,
    lpPairing_eq_integral, lsmul_flip_apply, toSpanSingleton_apply]

Premises used: SchwartzMap.toLpCLM_apply, ContinuousLinearMap.toSpanSingleton_apply, ContinuousLinearMap.lpPairing_eq_integral, MeasureTheory.Lp.toTemperedDistribution, ContinuousLinearMap.lsmul_flip_apply, ContinuousLinearMap.toPointwiseConvergenceCLM_apply, ContinuousLinearMap.comp_apply
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : CompleteSpace F
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f : ↥(Lp F p μ)
g : 𝓢(E, ℂ)
h :
  Filter.EventuallyEq.{u_3, u_4} (β := F) (ae μ)
    (fun (a : E) ↦ (↑(↑(g.toLp (1 - p⁻¹)⁻¹ μ) : E →ₘ[μ] ℂ) : E → ℂ) a • (↑(↑f : E →ₘ[μ] F) : E → F) a) fun (a : E) ↦
    HSMul.hSMul (α := ℂ) ((g : (a : E) → ℂ) a : ℂ) ((↑(↑f : E →ₘ[μ] F) : E → F) a)
⊢ Eq.{u_4 + 1} (α := F)
    (∫ (x : E), (↑(↑(g.toLp (1 - p⁻¹)⁻¹ μ) : E →ₘ[μ] ℂ) : E → ℂ) x • (↑(↑f : E →ₘ[μ] F) : E → F) x ∂μ)
    (∫ (x : E), HSMul.hSMul (α := ℂ) ((g : (a : E) → ℂ) x : ℂ) ((↑(↑f : E →ₘ[μ] F) : E → F) x) ∂μ)

Tactic:
apply integral_congr_ae

Premises used: MeasureTheory.integral_congr_ae
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : CompleteSpace F
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f : ↥(Lp F p μ)
g : 𝓢(E, ℂ)
h :
  ∀ (x : E) (hg : (↑(↑(g.toLp (1 - p⁻¹)⁻¹ μ) : E →ₘ[μ] ℂ) : E → ℂ) x = (g : (a : E) → ℂ) x),
    (↑(↑(g.toLp (1 - p⁻¹)⁻¹ μ) : E →ₘ[μ] ℂ) : E → ℂ) x • (↑(↑f : E →ₘ[μ] F) : E → F) x =
      HSMul.hSMul (α := ℂ) ((g : (a : E) → ℂ) x : ℂ) ((↑(↑f : E →ₘ[μ] F) : E → F) x)
⊢ Filter.EventuallyEq.{u_3, u_4} (β := F) (ae μ)
    (fun (a : E) ↦ (↑(↑(g.toLp (1 - p⁻¹)⁻¹ μ) : E →ₘ[μ] ℂ) : E → ℂ) a • (↑(↑f : E →ₘ[μ] F) : E → F) a) fun (a : E) ↦
    HSMul.hSMul (α := ℂ) ((g : (a : E) → ℂ) a : ℂ) ((↑(↑f : E →ₘ[μ] F) : E → F) a)

Tactic:
filter_upwards [g.coeFn_toLp (1 - p⁻¹)⁻¹ μ] with x hg

Premises used: HSub.hSub, SchwartzMap.coeFn_toLp, Inv.inv, OfNat.ofNat
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : CompleteSpace F
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f : ↥(Lp F p μ)
g : 𝓢(E, ℂ)
x : E
hg : (↑(↑(g.toLp (1 - p⁻¹)⁻¹ μ) : E →ₘ[μ] ℂ) : E → ℂ) x = (g : (a : E) → ℂ) x
h h₁ :
  HSMul.hSMul (α := ℂ) ((g : (a : E) → ℂ) x : ℂ) ((↑(↑f : E →ₘ[μ] F) : E → F) x) =
    HSMul.hSMul (α := ℂ) ((g : (a : E) → ℂ) x : ℂ) ((↑(↑f : E →ₘ[μ] F) : E → F) x)
⊢ (↑(↑(g.toLp (1 - p⁻¹)⁻¹ μ) : E →ₘ[μ] ℂ) : E → ℂ) x • (↑(↑f : E →ₘ[μ] F) : E → F) x =
    HSMul.hSMul (α := ℂ) ((g : (a : E) → ℂ) x : ℂ) ((↑(↑f : E →ₘ[μ] F) : E → F) x)

Tactic:
rw [hg]
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : CompleteSpace F
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
inst_7 : SecondCountableTopology E
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f : 𝓢(E, F)
h :
  ∀ (g : 𝓢(E, ℂ)),
    Eq.{u_4 + 1} (α := F) ((toTemperedDistribution (f.toLp p μ) : (a : 𝓢(E, ℂ)) → F) g : F)
      ((((toTemperedDistributionCLM E F μ : (a : 𝓢(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F)) : (a : 𝓢(E, ℂ)) → F) g : F)
⊢ Eq (α := 𝓢'(E, F)) (toTemperedDistribution (f.toLp p μ))
    ((toTemperedDistributionCLM E F μ : (a : 𝓢(E, F)) → 𝓢'(E, F)) f)

Tactic:
ext g
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : CompleteSpace F
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
inst_7 : SecondCountableTopology E
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f : 𝓢(E, F)
g : 𝓢(E, ℂ)
h :
  Eq.{u_4 + 1} (α := F)
    (∫ (x : E), HSMul.hSMul (α := ℂ) ((g : (a : E) → ℂ) x : ℂ) ((↑(↑(f.toLp p μ) : E →ₘ[μ] F) : E → F) x) ∂μ)
    (∫ (x : E), HSMul.hSMul (α := ℂ) (β := F) ((g : (a : E) → ℂ) x : ℂ) ((f : (a : E) → F) x : F) ∂μ)
⊢ Eq.{u_4 + 1} (α := F) ((toTemperedDistribution (f.toLp p μ) : (a : 𝓢(E, ℂ)) → F) g : F)
    ((((toTemperedDistributionCLM E F μ : (a : 𝓢(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F)) : (a : 𝓢(E, ℂ)) → F) g : F)

Tactic:
simp only [Lp.toTemperedDistribution_apply, toTemperedDistributionCLM_apply_apply]

Premises used: SchwartzMap.toTemperedDistributionCLM_apply_apply, MeasureTheory.Lp.toTemperedDistribution_apply
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : CompleteSpace F
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
inst_7 : SecondCountableTopology E
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f : 𝓢(E, F)
g : 𝓢(E, ℂ)
h :
  Filter.EventuallyEq.{u_3, u_4} (β := F) (ae μ)
    (fun (a : E) ↦ HSMul.hSMul (α := ℂ) ((g : (a : E) → ℂ) a : ℂ) ((↑(↑(f.toLp p μ) : E →ₘ[μ] F) : E → F) a))
    fun (a : E) ↦ HSMul.hSMul (α := ℂ) (β := F) ((g : (a : E) → ℂ) a : ℂ) ((f : (a : E) → F) a : F)
⊢ Eq.{u_4 + 1} (α := F)
    (∫ (x : E), HSMul.hSMul (α := ℂ) ((g : (a : E) → ℂ) x : ℂ) ((↑(↑(f.toLp p μ) : E →ₘ[μ] F) : E → F) x) ∂μ)
    (∫ (x : E), HSMul.hSMul (α := ℂ) (β := F) ((g : (a : E) → ℂ) x : ℂ) ((f : (a : E) → F) x : F) ∂μ)

Tactic:
apply integral_congr_ae

Premises used: MeasureTheory.integral_congr_ae
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : CompleteSpace F
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
inst_7 : SecondCountableTopology E
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f : 𝓢(E, F)
g : 𝓢(E, ℂ)
h :
  ∀ (x : E) (hf : (↑(↑(f.toLp p μ) : E →ₘ[μ] F) : E → F) x = (f : (a : E) → F) x),
    HSMul.hSMul (α := ℂ) ((g : (a : E) → ℂ) x : ℂ) ((↑(↑(f.toLp p μ) : E →ₘ[μ] F) : E → F) x) =
      HSMul.hSMul (α := ℂ) (β := F) ((g : (a : E) → ℂ) x : ℂ) ((f : (a : E) → F) x : F)
⊢ Filter.EventuallyEq.{u_3, u_4} (β := F) (ae μ)
    (fun (a : E) ↦ HSMul.hSMul (α := ℂ) ((g : (a : E) → ℂ) a : ℂ) ((↑(↑(f.toLp p μ) : E →ₘ[μ] F) : E → F) a))
    fun (a : E) ↦ HSMul.hSMul (α := ℂ) (β := F) ((g : (a : E) → ℂ) a : ℂ) ((f : (a : E) → F) a : F)

Tactic:
filter_upwards [f.coeFn_toLp p μ] with x hf

Premises used: SchwartzMap.coeFn_toLp
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : CompleteSpace F
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
inst_7 : SecondCountableTopology E
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f : 𝓢(E, F)
g : 𝓢(E, ℂ)
x : E
hf : (↑(↑(f.toLp p μ) : E →ₘ[μ] F) : E → F) x = (f : (a : E) → F) x
h h₁ :
  HSMul.hSMul (α := ℂ) (β := F) ((g : (a : E) → ℂ) x : ℂ) ((f : (a : E) → F) x : F) =
    HSMul.hSMul (α := ℂ) (β := F) ((g : (a : E) → ℂ) x : ℂ) ((f : (a : E) → F) x : F)
⊢ HSMul.hSMul (α := ℂ) ((g : (a : E) → ℂ) x : ℂ) ((↑(↑(f.toLp p μ) : E →ₘ[μ] F) : E → F) x) =
    HSMul.hSMul (α := ℂ) (β := F) ((g : (a : E) → ℂ) x : ℂ) ((f : (a : E) → F) x : F)

Tactic:
rw [hf]
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
F₁ : Type u_5
F₂ : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : CompleteSpace F
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
μ_1 : Measure E
hμ : μ_1.HasTemperateGrowth
μ : Measure E
inst_7 : μ.HasTemperateGrowth
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f g : ↥(Lp F p μ)
⊢ toTemperedDistribution (f + g) = HAdd.hAdd (α := 𝓢'(E, F)) (toTemperedDistribution f) (toTemperedDistribution g)

Tactic:
simp [Lp.toTemperedDistribution]

Premises used: MeasureTheory.Lp.toTemperedDistribution
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
F₁ : Type u_5
F₂ : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : CompleteSpace F
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
μ_1 : Measure E
hμ : μ_1.HasTemperateGrowth
μ : Measure E
inst_7 : μ.HasTemperateGrowth
p : ℝ≥0∞
hp : Fact (1 ≤ p)
a : ℂ
f : ↥(Lp F p μ)
⊢ toTemperedDistribution (a • f) =
    HSMul.hSMul (α := ℂ) (β := 𝓢'(E, F)) ((RingHom.id ℂ : (a : ℂ) → ℂ) a : ℂ) (toTemperedDistribution f)

Tactic:
simp [Lp.toTemperedDistribution]

Premises used: MeasureTheory.Lp.toTemperedDistribution
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
F₁ : Type u_5
F₂ : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : CompleteSpace F
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
μ_1 : Measure E
hμ : μ_1.HasTemperateGrowth
μ : Measure E
inst_7 : μ.HasTemperateGrowth
p : ℝ≥0∞
hp : Fact (1 ≤ p)
h : ∀ (x : 𝓢(E, ℂ)), Continuous (Y := F) fun (x_1 : ↥(Lp F p μ)) ↦ (toTemperedDistribution x_1 : (a : 𝓢(E, ℂ)) → F) x
⊢ Continuous (X := ↥(Lp F p μ)) (Y := 𝓢'(E, F)) toTemperedDistribution

Tactic:
apply PointwiseConvergenceCLM.continuous_of_continuous_eval

Premises used: PointwiseConvergenceCLM.continuous_of_continuous_eval
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
F₁ : Type u_5
F₂ : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : CompleteSpace F
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
μ_1 : Measure E
hμ : μ_1.HasTemperateGrowth
μ : Measure E
inst_7 : μ.HasTemperateGrowth
p : ℝ≥0∞
hp : Fact (1 ≤ p)
g : 𝓢(E, ℂ)
⊢ Fact (1 ≤ (1 - p⁻¹)⁻¹)

Tactic:
simp [fact_iff]

Premises used: fact_iff
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
F₁ : Type u_5
F₂ : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : CompleteSpace F
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
μ_1 : Measure E
hμ : μ_1.HasTemperateGrowth
μ : Measure E
inst_7 : μ.HasTemperateGrowth
p : ℝ≥0∞
hp : Fact (1 ≤ p)
g : 𝓢(E, ℂ)
⊢ Fact (1 ≤ (1 - p⁻¹)⁻¹)

Tactic:
haveI : Fact (1 ≤ (1 - p⁻¹)⁻¹) := by simp [fact_iff]
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
F₁ : Type u_5
F₂ : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : CompleteSpace F
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
μ_1 : Measure E
hμ : μ_1.HasTemperateGrowth
μ : Measure E
inst_7 : μ.HasTemperateGrowth
p : ℝ≥0∞
hp : Fact (1 ≤ p)
g : 𝓢(E, ℂ)
this : Fact (1 ≤ (1 - p⁻¹)⁻¹)
⊢ p.HolderConjugate (1 - p⁻¹)⁻¹

Tactic:
have hpq : ENNReal.HolderConjugate p (1 - p⁻¹)⁻¹ :=
      ENNReal.HolderConjugate.inv_one_sub_inv' hp.out
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
F₁ : Type u_5
F₂ : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : CompleteSpace F
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
μ_1 : Measure E
hμ : μ_1.HasTemperateGrowth
μ : Measure E
inst_7 : μ.HasTemperateGrowth
p : ℝ≥0∞
hp : Fact (1 ≤ p)
g : 𝓢(E, ℂ)
this : Fact (1 ≤ (1 - p⁻¹)⁻¹)
hpq : p.HolderConjugate (1 - p⁻¹)⁻¹
⊢ Continuous (Y := F) fun (x : ↥(Lp F p μ)) ↦ (toTemperedDistribution x : (a : 𝓢(E, ℂ)) → F) g

Tactic:
(((lsmul ℂ ℂ (E := F)).flip.lpPairing μ p (1 - p⁻¹)⁻¹).flip (g.toLp (1 - p⁻¹)⁻¹ μ)).cont

Premises used: HSub.hSub, Inv.inv, SchwartzMap.toLp, ContinuousLinearMap.flip, MeasureTheory.MemLp.toLp, ContinuousLinearMap.cont, ContinuousLinearMap.lpPairing, Complex, ContinuousLinearMap.lsmul, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
F₁ : Type u_5
F₂ : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : CompleteSpace F
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
μ_1 : Measure E
hμ : μ_1.HasTemperateGrowth
μ : Measure E
inst_7 : μ.HasTemperateGrowth
p : ℝ≥0∞
hp : Fact (1 ≤ p)
g : 𝓢(E, ℂ)
this : Fact (1 ≤ (1 - p⁻¹)⁻¹)
hpq : p.HolderConjugate (1 - p⁻¹)⁻¹
⊢ Continuous (Y := F) fun (x : ↥(Lp F p μ)) ↦ (toTemperedDistribution x : (a : 𝓢(E, ℂ)) → F) g

Tactic:
exact (((lsmul ℂ ℂ (E := F)).flip.lpPairing μ p (1 - p⁻¹)⁻¹).flip (g.toLp (1 - p⁻¹)⁻¹ μ)).cont

Premises used: HSub.hSub, Inv.inv, SchwartzMap.toLp, ContinuousLinearMap.flip, ContinuousLinearMap.cont, ContinuousLinearMap.lpPairing, Complex, ContinuousLinearMap.lsmul, OfNat.ofNat, DFunLike.coe