awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
E : Type u_4
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : FiniteDimensional ℝ E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p : ℝ
hp_1 : Real.HolderConjugate (↑(finrank ℝ E) : ℝ) p
C : ℝ≥0 := lintegralPowLePowLIntegralFDerivConst μ p
ι : Type := Fin (finrank ℝ E)
hιcard : #ι = finrank ℝ E
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃L[ℝ] ι → ℝ := ContinuousLinearEquiv.ofFinrankEq this
hp : Real.HolderConjugate (↑#ι : ℝ) p
h0p : 0 ≤ p
c : ℝ≥0 := μ.addHaarScalarFactor (Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume)
hc : 0 < c
h2c : μ = HSMul.hSMul (β := Measure E) c (Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume)
simp_rw : ¬(↑c : ℝ≥0∞) = 0
simp_rw₁ : ¬c = 0
⊢ (↑c : ℝ≥0∞) ≠ 0
have simp_rw₂ : ¬False
Tactic: simp_rw [ne_eq, ENNReal.coe_eq_zero, hc.ne', not_false_eq_true]
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (hypothesis)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
E : Type u_4
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : FiniteDimensional ℝ E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p : ℝ
hp_1 : Real.HolderConjugate (↑(finrank ℝ E) : ℝ) p
C : ℝ≥0 := lintegralPowLePowLIntegralFDerivConst μ p
ι : Type := Fin (finrank ℝ E)
hιcard : #ι = finrank ℝ E
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃L[ℝ] ι → ℝ := ContinuousLinearEquiv.ofFinrankEq this
hp : Real.HolderConjugate (↑#ι : ℝ) p
h0p : 0 ≤ p
c : ℝ≥0 := μ.addHaarScalarFactor (Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume)
hc : 0 < c
h2c : μ = HSMul.hSMul (β := Measure E) c (Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume)
⊢ ∫⁻ (x : E), ‖u x‖ₑ ^ p ∂μ ≤ (↑C : ℝ≥0∞) * (∫⁻ (x : E), enorm (E := E →L[ℝ] F) (fderiv ℝ u x) ∂μ) ^ p
have h3c : (↑c : ℝ≥0∞) ≠ 0
Tactic: have h3c : (c : ℝ≥0∞) ≠ 0 := by simp_rw [ne_eq, ENNReal.coe_eq_zero, hc.ne', not_false_eq_true]
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (hypothesis)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
E : Type u_4
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : FiniteDimensional ℝ E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p : ℝ
hp_1 : Real.HolderConjugate (↑(finrank ℝ E) : ℝ) p
C : ℝ≥0 := lintegralPowLePowLIntegralFDerivConst μ p
ι : Type := Fin (finrank ℝ E)
hιcard : #ι = finrank ℝ E
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃L[ℝ] ι → ℝ := ContinuousLinearEquiv.ofFinrankEq this
hp : Real.HolderConjugate (↑#ι : ℝ) p
h0p : 0 ≤ p
c : ℝ≥0 := μ.addHaarScalarFactor (Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume)
hc : 0 < c
h2c : μ = HSMul.hSMul (β := Measure E) c (Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume)
h3c : (↑c : ℝ≥0∞) ≠ 0
⊢ ∫⁻ (x : E), ‖u x‖ₑ ^ p ∂μ ≤ (↑C : ℝ≥0∞) * (∫⁻ (x : E), enorm (E := E →L[ℝ] F) (fderiv ℝ u x) ∂μ) ^ p
have h0C : C = c * ‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p * (c ^ p)⁻¹
Tactic: have h0C : C = (c * ‖(e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p) * (c ^ p)⁻¹ := by
    simp_rw [c, ι, C, e, lintegralPowLePowLIntegralFDerivConst]
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
E : Type u_4
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : FiniteDimensional ℝ E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p : ℝ
hp_1 : Real.HolderConjugate (↑(finrank ℝ E) : ℝ) p
C : ℝ≥0 := lintegralPowLePowLIntegralFDerivConst μ p
ι : Type := Fin (finrank ℝ E)
hιcard : #ι = finrank ℝ E
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃L[ℝ] ι → ℝ := ContinuousLinearEquiv.ofFinrankEq this
hp : Real.HolderConjugate (↑#ι : ℝ) p
h0p : 0 ≤ p
c : ℝ≥0 := μ.addHaarScalarFactor (Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume)
hc : 0 < c
h2c : μ = HSMul.hSMul (β := Measure E) c (Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume)
h3c : (↑c : ℝ≥0∞) ≠ 0
h0C : C = c * ‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p * (c ^ p)⁻¹
⊢ C * c ^ p = c * ‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p
have rw : c * ‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p * (c ^ p)⁻¹ * c ^ p = c * ‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p
Tactic: rw [h0C, inv_mul_cancel_right₀ (NNReal.rpow_pos hc).ne']
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
E : Type u_4
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : FiniteDimensional ℝ E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p : ℝ
hp_1 : Real.HolderConjugate (↑(finrank ℝ E) : ℝ) p
C : ℝ≥0 := lintegralPowLePowLIntegralFDerivConst μ p
ι : Type := Fin (finrank ℝ E)
hιcard : #ι = finrank ℝ E
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃L[ℝ] ι → ℝ := ContinuousLinearEquiv.ofFinrankEq this
hp : Real.HolderConjugate (↑#ι : ℝ) p
h0p : 0 ≤ p
c : ℝ≥0 := μ.addHaarScalarFactor (Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume)
hc : 0 < c
h2c : μ = HSMul.hSMul (β := Measure E) c (Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume)
h3c : (↑c : ℝ≥0∞) ≠ 0
h0C : C = c * ‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p * (c ^ p)⁻¹
rw : c * ‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p * (c ^ p)⁻¹ * c ^ p = c * ‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p
⊢ C * c ^ p = c * ‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p
have rw₁ : c * ‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p = c * ‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p
Tactic: rw [h0C, inv_mul_cancel_right₀ (NNReal.rpow_pos hc).ne']
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (hypothesis)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
E : Type u_4
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : FiniteDimensional ℝ E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p : ℝ
hp_1 : Real.HolderConjugate (↑(finrank ℝ E) : ℝ) p
C : ℝ≥0 := lintegralPowLePowLIntegralFDerivConst μ p
ι : Type := Fin (finrank ℝ E)
hιcard : #ι = finrank ℝ E
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃L[ℝ] ι → ℝ := ContinuousLinearEquiv.ofFinrankEq this
hp : Real.HolderConjugate (↑#ι : ℝ) p
h0p : 0 ≤ p
c : ℝ≥0 := μ.addHaarScalarFactor (Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume)
hc : 0 < c
h2c : μ = HSMul.hSMul (β := Measure E) c (Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume)
h3c : (↑c : ℝ≥0∞) ≠ 0
h0C : C = c * ‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p * (c ^ p)⁻¹
⊢ ∫⁻ (x : E), ‖u x‖ₑ ^ p ∂μ ≤ (↑C : ℝ≥0∞) * (∫⁻ (x : E), enorm (E := E →L[ℝ] F) (fderiv ℝ u x) ∂μ) ^ p
have hC : C * c ^ p = c * ‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p
Tactic: have hC : C * c ^ p = c * ‖(e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p := by
    rw [h0C, inv_mul_cancel_right₀ (NNReal.rpow_pos hc).ne']
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
E : Type u_4
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : FiniteDimensional ℝ E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p : ℝ
hp_1 : Real.HolderConjugate (↑(finrank ℝ E) : ℝ) p
C : ℝ≥0 := lintegralPowLePowLIntegralFDerivConst μ p
ι : Type := Fin (finrank ℝ E)
hιcard : #ι = finrank ℝ E
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃L[ℝ] ι → ℝ := ContinuousLinearEquiv.ofFinrankEq this
hp : Real.HolderConjugate (↑#ι : ℝ) p
h0p : 0 ≤ p
c : ℝ≥0 := μ.addHaarScalarFactor (Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume)
hc : 0 < c
h2c : μ = HSMul.hSMul (β := Measure E) c (Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume)
h3c : (↑c : ℝ≥0∞) ≠ 0
h0C : C = c * ‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p * (c ^ p)⁻¹
hC : C * c ^ p = c * ‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p
⊢ ∫⁻ (x : E), ‖u x‖ₑ ^ p ∂μ ≤ (↑C : ℝ≥0∞) * (∫⁻ (x : E), enorm (E := E →L[ℝ] F) (fderiv ℝ u x) ∂μ) ^ p
have simp : (↑c : ℝ≥0∞) * ∫⁻ (x : E), ‖u x‖ₑ ^ p ∂Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume ≤
  (↑C : ℝ≥0∞) *
    ((↑c : ℝ≥0∞) *
        ∫⁻ (x : E),
          enorm (E := E →L[ℝ] F) (fderiv ℝ u x) ∂Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume) ^
      p
Tactic: simp only [h2c, ENNReal.smul_def, lintegral_smul_measure, smul_eq_mul]
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (hypothesis)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
E : Type u_4
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : FiniteDimensional ℝ E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p : ℝ
hp_1 : Real.HolderConjugate (↑(finrank ℝ E) : ℝ) p
C : ℝ≥0 := lintegralPowLePowLIntegralFDerivConst μ p
ι : Type := Fin (finrank ℝ E)
hιcard : #ι = finrank ℝ E
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃L[ℝ] ι → ℝ := ContinuousLinearEquiv.ofFinrankEq this
hp : Real.HolderConjugate (↑#ι : ℝ) p
h0p : 0 ≤ p
c : ℝ≥0 := μ.addHaarScalarFactor (Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume)
hc : 0 < c
h2c : μ = HSMul.hSMul (β := Measure E) c (Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume)
h3c : (↑c : ℝ≥0∞) ≠ 0
h0C : C = c * ‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p * (c ^ p)⁻¹
hC : C * c ^ p = c * ‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p
v : (ι → ℝ) → F := u ∘ (⇑e.symm : (a : ι → ℝ) → E)
⊢ (↑c : ℝ≥0∞) * ∫⁻ (x : E), ‖u x‖ₑ ^ p ∂Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume ≤
    (↑C : ℝ≥0∞) *
      ((↑c : ℝ≥0∞) *
          ∫⁻ (x : E),
            enorm (E := E →L[ℝ] F) (fderiv ℝ u x) ∂Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume) ^
        p
have hv : ContDiff ℝ 1 v
Tactic: have hv : ContDiff ℝ 1 v := hu.comp e.symm.contDiff
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (hypothesis)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
E : Type u_4
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : FiniteDimensional ℝ E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p : ℝ
hp_1 : Real.HolderConjugate (↑(finrank ℝ E) : ℝ) p
C : ℝ≥0 := lintegralPowLePowLIntegralFDerivConst μ p
ι : Type := Fin (finrank ℝ E)
hιcard : #ι = finrank ℝ E
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃L[ℝ] ι → ℝ := ContinuousLinearEquiv.ofFinrankEq this
hp : Real.HolderConjugate (↑#ι : ℝ) p
h0p : 0 ≤ p
c : ℝ≥0 := μ.addHaarScalarFactor (Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume)
hc : 0 < c
h2c : μ = HSMul.hSMul (β := Measure E) c (Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume)
h3c : (↑c : ℝ≥0∞) ≠ 0
h0C : C = c * ‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p * (c ^ p)⁻¹
hC : C * c ^ p = c * ‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p
v : (ι → ℝ) → F := u ∘ (⇑e.symm : (a : ι → ℝ) → E)
hv : ContDiff ℝ 1 v
⊢ (↑c : ℝ≥0∞) * ∫⁻ (x : E), ‖u x‖ₑ ^ p ∂Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume ≤
    (↑C : ℝ≥0∞) *
      ((↑c : ℝ≥0∞) *
          ∫⁻ (x : E),
            enorm (E := E →L[ℝ] F) (fderiv ℝ u x) ∂Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume) ^
        p
have h2v : HasCompactSupport v
Tactic: have h2v : HasCompactSupport v := h2u.comp_homeomorph e.symm.toHomeomorph
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
E : Type u_4
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : FiniteDimensional ℝ E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p : ℝ
hp_1 : Real.HolderConjugate (↑(finrank ℝ E) : ℝ) p
C : ℝ≥0 := lintegralPowLePowLIntegralFDerivConst μ p
ι : Type := Fin (finrank ℝ E)
hιcard : #ι = finrank ℝ E
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃L[ℝ] ι → ℝ := ContinuousLinearEquiv.ofFinrankEq this
hp : Real.HolderConjugate (↑#ι : ℝ) p
h0p : 0 ≤ p
c : ℝ≥0 := μ.addHaarScalarFactor (Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume)
hc : 0 < c
h2c : μ = HSMul.hSMul (β := Measure E) c (Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume)
h3c : (↑c : ℝ≥0∞) ≠ 0
h0C : C = c * ‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p * (c ^ p)⁻¹
hC : C * c ^ p = c * ‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p
v : (ι → ℝ) → F := u ∘ (⇑e.symm : (a : ι → ℝ) → E)
hv : ContDiff ℝ 1 v
h2v : HasCompactSupport v
⊢ ∫⁻ (x : E), ‖u x‖ₑ ^ p ∂Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume = ∫⁻ (y : ι → ℝ), ‖v y‖ₑ ^ p
have refine : Measurable (β := ℝ≥0∞) fun (x : E) ↦ ‖u x‖ₑ ^ p
Tactic: refine lintegral_map ?_ e.symm.continuous.measurable
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (hypothesis)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
E : Type u_4
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : FiniteDimensional ℝ E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p : ℝ
hp_1 : Real.HolderConjugate (↑(finrank ℝ E) : ℝ) p
C : ℝ≥0 := lintegralPowLePowLIntegralFDerivConst μ p
ι : Type := Fin (finrank ℝ E)
hιcard : #ι = finrank ℝ E
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃L[ℝ] ι → ℝ := ContinuousLinearEquiv.ofFinrankEq this
hp : Real.HolderConjugate (↑#ι : ℝ) p
h0p : 0 ≤ p
c : ℝ≥0 := μ.addHaarScalarFactor (Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume)
hc : 0 < c
h2c : μ = HSMul.hSMul (β := Measure E) c (Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume)
h3c : (↑c : ℝ≥0∞) ≠ 0
h0C : C = c * ‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p * (c ^ p)⁻¹
hC : C * c ^ p = c * ‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p
v : (ι → ℝ) → F := u ∘ (⇑e.symm : (a : ι → ℝ) → E)
hv : ContDiff ℝ 1 v
h2v : HasCompactSupport v
⊢ Measurable (β := ℝ≥0∞) fun (x : E) ↦ ‖u x‖ₑ ^ p
have this₁ : let this := borel F;
BorelSpace F
Tactic: borelize F
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
E : Type u_4
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : FiniteDimensional ℝ E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p : ℝ
hp_1 : Real.HolderConjugate (↑(finrank ℝ E) : ℝ) p
C : ℝ≥0 := lintegralPowLePowLIntegralFDerivConst μ p
ι : Type := Fin (finrank ℝ E)
hιcard : #ι = finrank ℝ E
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃L[ℝ] ι → ℝ := ContinuousLinearEquiv.ofFinrankEq this
hp : Real.HolderConjugate (↑#ι : ℝ) p
h0p : 0 ≤ p
c : ℝ≥0 := μ.addHaarScalarFactor (Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume)
hc : 0 < c
h2c : μ = HSMul.hSMul (β := Measure E) c (Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume)
h3c : (↑c : ℝ≥0∞) ≠ 0
h0C : C = c * ‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p * (c ^ p)⁻¹
hC : C * c ^ p = c * ‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p
v : (ι → ℝ) → F := u ∘ (⇑e.symm : (a : ι → ℝ) → E)
hv : ContDiff ℝ 1 v
h2v : HasCompactSupport v
⊢ (∫⁻ (y : ι → ℝ), enorm (E := (ι → ℝ) →L[ℝ] F) (fderiv ℝ v y)) ^ p =
    (∫⁻ (y : ι → ℝ),
        enorm (E := (ι → ℝ) →L[ℝ] F)
          (fderiv ℝ u ((e.symm : (a : ι → ℝ) → E) y) ∘SL fderiv ℝ (⇑e.symm : (a : ι → ℝ) → E) y)) ^
      p
have h : ∀ (y : ι → ℝ),
  Eq (α := (ι → ℝ) →L[ℝ] F) (fderiv ℝ v y)
    (fderiv ℝ u ((e.symm : (a : ι → ℝ) → E) y) ∘SL fderiv ℝ (⇑e.symm : (a : ι → ℝ) → E) y)
Tactic: congr! with y
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
E : Type u_4
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : FiniteDimensional ℝ E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p : ℝ
hp_1 : Real.HolderConjugate (↑(finrank ℝ E) : ℝ) p
C : ℝ≥0 := lintegralPowLePowLIntegralFDerivConst μ p
ι : Type := Fin (finrank ℝ E)
hιcard : #ι = finrank ℝ E
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃L[ℝ] ι → ℝ := ContinuousLinearEquiv.ofFinrankEq this
hp : Real.HolderConjugate (↑#ι : ℝ) p
h0p : 0 ≤ p
c : ℝ≥0 := μ.addHaarScalarFactor (Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume)
hc : 0 < c
h2c : μ = HSMul.hSMul (β := Measure E) c (Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume)
h3c : (↑c : ℝ≥0∞) ≠ 0
h0C : C = c * ‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p * (c ^ p)⁻¹
hC : C * c ^ p = c * ‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p
v : (ι → ℝ) → F := u ∘ (⇑e.symm : (a : ι → ℝ) → E)
hv : ContDiff ℝ 1 v
h2v : HasCompactSupport v
y : ι → ℝ
⊢ Eq (α := (ι → ℝ) →L[ℝ] F) (fderiv ℝ v y)
    (fderiv ℝ u ((e.symm : (a : ι → ℝ) → E) y) ∘SL fderiv ℝ (⇑e.symm : (a : ι → ℝ) → E) y)
have h : DifferentiableAt ℝ (F := E) (⇑e.symm : (a : ι → ℝ) → E) y
Tactic: apply fderiv_comp _ (hu.differentiable one_ne_zero _)
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
E : Type u_4
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : FiniteDimensional ℝ E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p : ℝ
hp_1 : Real.HolderConjugate (↑(finrank ℝ E) : ℝ) p
C : ℝ≥0 := lintegralPowLePowLIntegralFDerivConst μ p
ι : Type := Fin (finrank ℝ E)
hιcard : #ι = finrank ℝ E
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃L[ℝ] ι → ℝ := ContinuousLinearEquiv.ofFinrankEq this
hp : Real.HolderConjugate (↑#ι : ℝ) p
h0p : 0 ≤ p
c : ℝ≥0 := μ.addHaarScalarFactor (Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume)
hc : 0 < c
h2c : μ = HSMul.hSMul (β := Measure E) c (Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume)
h3c : (↑c : ℝ≥0∞) ≠ 0
h0C : C = c * ‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p * (c ^ p)⁻¹
hC : C * c ^ p = c * ‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p
v : (ι → ℝ) → F := u ∘ (⇑e.symm : (a : ι → ℝ) → E)
hv : ContDiff ℝ 1 v
h2v : HasCompactSupport v
⊢ (∫⁻ (y : ι → ℝ),
        enorm (E := (ι → ℝ) →L[ℝ] F)
          (fderiv ℝ u ((e.symm : (a : ι → ℝ) → E) y) ∘SL fderiv ℝ (⇑e.symm : (a : ι → ℝ) → E) y)) ^
      p ≤
    (∫⁻ (y : ι → ℝ),
        enorm (E := E →L[ℝ] F) (fderiv ℝ u ((e.symm : (a : ι → ℝ) → E) y)) * ‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖ₑ) ^
      p
have h₁ : ∀ (y : ι → ℝ),
  enorm (E := (ι → ℝ) →L[ℝ] F) (fderiv ℝ u ((e.symm : (a : ι → ℝ) → E) y) ∘SL fderiv ℝ (⇑e.symm : (a : ι → ℝ) → E) y) ≤
    enorm (E := E →L[ℝ] F) (fderiv ℝ u ((e.symm : (a : ι → ℝ) → E) y)) * ‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖ₑ
Tactic: gcongr with y
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
E : Type u_4
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : FiniteDimensional ℝ E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p : ℝ
hp_1 : Real.HolderConjugate (↑(finrank ℝ E) : ℝ) p
C : ℝ≥0 := lintegralPowLePowLIntegralFDerivConst μ p
ι : Type := Fin (finrank ℝ E)
hιcard : #ι = finrank ℝ E
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃L[ℝ] ι → ℝ := ContinuousLinearEquiv.ofFinrankEq this
hp : Real.HolderConjugate (↑#ι : ℝ) p
h0p : 0 ≤ p
c : ℝ≥0 := μ.addHaarScalarFactor (Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume)
hc : 0 < c
h2c : μ = HSMul.hSMul (β := Measure E) c (Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume)
h3c : (↑c : ℝ≥0∞) ≠ 0
h0C : C = c * ‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p * (c ^ p)⁻¹
hC : C * c ^ p = c * ‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p
v : (ι → ℝ) → F := u ∘ (⇑e.symm : (a : ι → ℝ) → E)
hv : ContDiff ℝ 1 v
h2v : HasCompactSupport v
y : ι → ℝ
⊢ enorm (E := (ι → ℝ) →L[ℝ] F) (fderiv ℝ u ((e.symm : (a : ι → ℝ) → E) y) ∘SL fderiv ℝ (⇑e.symm : (a : ι → ℝ) → E) y) ≤
    enorm (E := E →L[ℝ] F) (fderiv ℝ u ((e.symm : (a : ι → ℝ) → E) y)) * ‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖ₑ
have h₁ : enorm (E := (ι → ℝ) →L[ℝ] F) (fderiv ℝ u ((e.symm : (a : ι → ℝ) → E) y) ∘SL (↑e.symm : (ι → ℝ) →L[ℝ] E)) ≤
  enorm (E := E →L[ℝ] F) (fderiv ℝ u ((e.symm : (a : ι → ℝ) → E) y)) * ‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖ₑ
Tactic: rw [e.symm.fderiv]
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
E : Type u_4
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : FiniteDimensional ℝ E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p : ℝ
hp_1 : Real.HolderConjugate (↑(finrank ℝ E) : ℝ) p
C : ℝ≥0 := lintegralPowLePowLIntegralFDerivConst μ p
ι : Type := Fin (finrank ℝ E)
hιcard : #ι = finrank ℝ E
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃L[ℝ] ι → ℝ := ContinuousLinearEquiv.ofFinrankEq this
hp : Real.HolderConjugate (↑#ι : ℝ) p
h0p : 0 ≤ p
c : ℝ≥0 := μ.addHaarScalarFactor (Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume)
hc : 0 < c
h2c : μ = HSMul.hSMul (β := Measure E) c (Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume)
h3c : (↑c : ℝ≥0∞) ≠ 0
h0C : C = c * ‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p * (c ^ p)⁻¹
hC : C * c ^ p = c * ‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p
v : (ι → ℝ) → F := u ∘ (⇑e.symm : (a : ι → ℝ) → E)
hv : ContDiff ℝ 1 v
h2v : HasCompactSupport v
⊢ (∫⁻ (y : ι → ℝ),
        enorm (E := E →L[ℝ] F) (fderiv ℝ u ((e.symm : (a : ι → ℝ) → E) y)) * ‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖ₑ) ^
      p =
    (‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖ₑ *
        ∫⁻ (y : ι → ℝ), enorm (E := E →L[ℝ] F) (fderiv ℝ u ((e.symm : (a : ι → ℝ) → E) y))) ^
      p
have hf : Measurable (β := ℝ≥0∞) fun (y : ι → ℝ) ↦ enorm (E := E →L[ℝ] F) (fderiv ℝ u ((e.symm : (a : ι → ℝ) → E) y))
Tactic: rw [lintegral_mul_const, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
E : Type u_4
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : FiniteDimensional ℝ E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p : ℝ
hp_1 : Real.HolderConjugate (↑(finrank ℝ E) : ℝ) p
C : ℝ≥0 := lintegralPowLePowLIntegralFDerivConst μ p
ι : Type := Fin (finrank ℝ E)
hιcard : #ι = finrank ℝ E
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃L[ℝ] ι → ℝ := ContinuousLinearEquiv.ofFinrankEq this
hp : Real.HolderConjugate (↑#ι : ℝ) p
h0p : 0 ≤ p
c : ℝ≥0 := μ.addHaarScalarFactor (Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume)
hc : 0 < c
h2c : μ = HSMul.hSMul (β := Measure E) c (Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume)
h3c : (↑c : ℝ≥0∞) ≠ 0
h0C : C = c * ‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p * (c ^ p)⁻¹
hC : C * c ^ p = c * ‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p
v : (ι → ℝ) → F := u ∘ (⇑e.symm : (a : ι → ℝ) → E)
hv : ContDiff ℝ 1 v
h2v : HasCompactSupport v
⊢ Measurable (β := ℝ≥0∞) fun (y : ι → ℝ) ↦ enorm (E := E →L[ℝ] F) (fderiv ℝ u ((e.symm : (a : ι → ℝ) → E) y))
have funProp : FinStronglyMeasurable (β := E →L[ℝ] F) (fun (x11 : E) ↦ fderiv ℝ u x11) ?μ
Tactic: fun_prop