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)
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
funProp : FinStronglyMeasurable (β := E →L[ℝ] F) (fun (x11 : E) ↦ fderiv ℝ u x11) ?μ
⊢ Measurable (β := ℝ≥0∞) fun (y : ι → ℝ) ↦ enorm (E := E →L[ℝ] F) (fderiv ℝ u ((e.symm : (a : ι → ℝ) → E) y))
have funProp₁ : inst_4 ≤ inst_4
Tactic: fun_prop
-- 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
funProp : FinStronglyMeasurable (β := E →L[ℝ] F) (fun (x11 : E) ↦ fderiv ℝ u x11) ?μ
funProp₁ : inst_4 ≤ inst_4
⊢ Measurable (β := ℝ≥0∞) fun (y : ι → ℝ) ↦ enorm (E := E →L[ℝ] F) (fderiv ℝ u ((e.symm : (a : ι → ℝ) → E) y))
have funProp₂ : MeasurableEmbedding (β := E →L[ℝ] F) fun (y11 : E) ↦ fderiv ℝ u y11
Tactic: fun_prop
-- 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
funProp : FinStronglyMeasurable (β := E →L[ℝ] F) (fun (x11 : E) ↦ fderiv ℝ u x11) ?μ
funProp₁ : inst_4 ≤ inst_4
funProp₂ : MeasurableEmbedding (β := E →L[ℝ] F) fun (y11 : E) ↦ fderiv ℝ u y11
⊢ Measurable (β := ℝ≥0∞) fun (y : ι → ℝ) ↦ enorm (E := E →L[ℝ] F) (fderiv ℝ u ((e.symm : (a : ι → ℝ) → E) y))
have funProp₃ : LE.le (α := MeasurableSpace (ι → ℝ)) (MeasurableSpace.pi (X := fun (a : ι) ↦ ℝ)) MeasureSpace.toMeasurableSpace
Tactic: fun_prop
-- 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
funProp : FinStronglyMeasurable (β := E →L[ℝ] F) (fun (x11 : E) ↦ fderiv ℝ u x11) ?μ
funProp₁ : inst_4 ≤ inst_4
funProp₂ : MeasurableEmbedding (β := E →L[ℝ] F) fun (y11 : E) ↦ fderiv ℝ u y11
funProp₃ :
  LE.le (α := MeasurableSpace (ι → ℝ)) (MeasurableSpace.pi (X := fun (a : ι) ↦ ℝ)) MeasureSpace.toMeasurableSpace
⊢ Measurable (β := ℝ≥0∞) fun (y : ι → ℝ) ↦ enorm (E := E →L[ℝ] F) (fderiv ℝ u ((e.symm : (a : ι → ℝ) → E) y))
have funProp₄ : MeasurableEmbedding.{0, u_4} (β := E) fun (y : ι → ℝ) ↦ (e.symm : (a : ι → ℝ) → E) y
Tactic: fun_prop
-- 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
⊢ (‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖ₑ *
        ∫⁻ (y : ι → ℝ), enorm (E := E →L[ℝ] F) (fderiv ℝ u ((e.symm : (a : ι → ℝ) → E) y))) ^
      p =
    (↑(‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p) : ℝ≥0∞) *
      (∫⁻ (y : ι → ℝ), enorm (E := E →L[ℝ] F) (fderiv ℝ u ((e.symm : (a : ι → ℝ) → E) y))) ^ p
have rw : ‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖ₑ ^ p *
    (∫⁻ (y : ι → ℝ), enorm (E := E →L[ℝ] F) (fderiv ℝ u ((e.symm : (a : ι → ℝ) → E) y))) ^ p =
  (↑(‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p) : ℝ≥0∞) *
    (∫⁻ (y : ι → ℝ), enorm (E := E →L[ℝ] F) (fderiv ℝ u ((e.symm : (a : ι → ℝ) → E) y))) ^ p
Tactic: rw [ENNReal.mul_rpow_of_nonneg _ _ h0p, enorm_eq_nnnorm, ← ENNReal.coe_rpow_of_nonneg _ h0p]
-- 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
rw :
  ‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖ₑ ^ p *
      (∫⁻ (y : ι → ℝ), enorm (E := E →L[ℝ] F) (fderiv ℝ u ((e.symm : (a : ι → ℝ) → E) y))) ^ p =
    (↑(‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p) : ℝ≥0∞) *
      (∫⁻ (y : ι → ℝ), enorm (E := E →L[ℝ] F) (fderiv ℝ u ((e.symm : (a : ι → ℝ) → E) y))) ^ p
⊢ (‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖ₑ *
        ∫⁻ (y : ι → ℝ), enorm (E := E →L[ℝ] F) (fderiv ℝ u ((e.symm : (a : ι → ℝ) → E) y))) ^
      p =
    (↑(‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p) : ℝ≥0∞) *
      (∫⁻ (y : ι → ℝ), enorm (E := E →L[ℝ] F) (fderiv ℝ u ((e.symm : (a : ι → ℝ) → E) y))) ^ p
have rw₁ : (↑‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ : ℝ≥0∞) ^ p *
    (∫⁻ (y : ι → ℝ), enorm (E := E →L[ℝ] F) (fderiv ℝ u ((e.symm : (a : ι → ℝ) → E) y))) ^ p =
  (↑(‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p) : ℝ≥0∞) *
    (∫⁻ (y : ι → ℝ), enorm (E := E →L[ℝ] F) (fderiv ℝ u ((e.symm : (a : ι → ℝ) → E) y))) ^ p
Tactic: rw [ENNReal.mul_rpow_of_nonneg _ _ h0p, enorm_eq_nnnorm, ← ENNReal.coe_rpow_of_nonneg _ h0p]
-- 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
rw :
  ‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖ₑ ^ p *
      (∫⁻ (y : ι → ℝ), enorm (E := E →L[ℝ] F) (fderiv ℝ u ((e.symm : (a : ι → ℝ) → E) y))) ^ p =
    (↑(‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p) : ℝ≥0∞) *
      (∫⁻ (y : ι → ℝ), enorm (E := E →L[ℝ] F) (fderiv ℝ u ((e.symm : (a : ι → ℝ) → E) y))) ^ p
rw₁ :
  (↑‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ : ℝ≥0∞) ^ p *
      (∫⁻ (y : ι → ℝ), enorm (E := E →L[ℝ] F) (fderiv ℝ u ((e.symm : (a : ι → ℝ) → E) y))) ^ p =
    (↑(‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p) : ℝ≥0∞) *
      (∫⁻ (y : ι → ℝ), enorm (E := E →L[ℝ] F) (fderiv ℝ u ((e.symm : (a : ι → ℝ) → E) y))) ^ p
⊢ (‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖ₑ *
        ∫⁻ (y : ι → ℝ), enorm (E := E →L[ℝ] F) (fderiv ℝ u ((e.symm : (a : ι → ℝ) → E) y))) ^
      p =
    (↑(‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p) : ℝ≥0∞) *
      (∫⁻ (y : ι → ℝ), enorm (E := E →L[ℝ] F) (fderiv ℝ u ((e.symm : (a : ι → ℝ) → E) y))) ^ p
have rw₂ : (↑(‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p) : ℝ≥0∞) *
    (∫⁻ (y : ι → ℝ), enorm (E := E →L[ℝ] F) (fderiv ℝ u ((e.symm : (a : ι → ℝ) → E) y))) ^ p =
  (↑(‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p) : ℝ≥0∞) *
    (∫⁻ (y : ι → ℝ), enorm (E := E →L[ℝ] F) (fderiv ℝ u ((e.symm : (a : ι → ℝ) → E) y))) ^ p
Tactic: rw [ENNReal.mul_rpow_of_nonneg _ _ h0p, enorm_eq_nnnorm, ← ENNReal.coe_rpow_of_nonneg _ h0p]
-- 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
⊢ (↑(‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p) : ℝ≥0∞) *
      (∫⁻ (y : ι → ℝ), enorm (E := E →L[ℝ] F) (fderiv ℝ u ((e.symm : (a : ι → ℝ) → E) y))) ^ p =
    (↑(‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p) : ℝ≥0∞) *
      (∫⁻ (x : E), enorm (E := E →L[ℝ] F) (fderiv ℝ u x) ∂Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume) ^
        p
have e_a : ∫⁻ (y : ι → ℝ), enorm (E := E →L[ℝ] F) (fderiv ℝ u ((e.symm : (a : ι → ℝ) → E) y)) =
  ∫⁻ (x : E), enorm (E := E →L[ℝ] F) (fderiv ℝ u x) ∂Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume
Tactic: congr
-- 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)) =
    ∫⁻ (x : E), enorm (E := E →L[ℝ] F) (fderiv ℝ u x) ∂Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume
have rw : Measurable (β := ℝ≥0∞) fun (x : E) ↦ enorm (E := E →L[ℝ] F) (fderiv ℝ u x)
Tactic: rw [lintegral_map _ e.symm.continuous.measurable]
-- 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 (x : E) ↦ enorm (E := E →L[ℝ] F) (fderiv ℝ u x)
have funProp : FinStronglyMeasurable (β := E →L[ℝ] F) (fun (x : E) ↦ fderiv ℝ u x) ?μ
Tactic: fun_prop
-- 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
funProp : FinStronglyMeasurable (β := E →L[ℝ] F) (fun (x : E) ↦ fderiv ℝ u x) ?μ
⊢ Measurable (β := ℝ≥0∞) fun (x : E) ↦ enorm (E := E →L[ℝ] F) (fderiv ℝ u x)
have funProp₁ : inst_4 ≤ inst_4
Tactic: fun_prop
-- 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
funProp : FinStronglyMeasurable (β := E →L[ℝ] F) (fun (x : E) ↦ fderiv ℝ u x) ?μ
funProp₁ : inst_4 ≤ inst_4
⊢ Measurable (β := ℝ≥0∞) fun (x : E) ↦ enorm (E := E →L[ℝ] F) (fderiv ℝ u x)
have funProp₂ : MeasurableEmbedding (β := E →L[ℝ] F) fun (x : E) ↦ fderiv ℝ u x
Tactic: fun_prop
-- 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
⊢ (↑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 this₁ : ∫⁻ (x : E), ‖u x‖ₑ ^ p ∂Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume ≤
  (↑(‖(↑e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p) : ℝ≥0∞) *
    (∫⁻ (x : E), enorm (E := E →L[ℝ] F) (fderiv ℝ u x) ∂Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume) ^ p
Tactic: have :=
  calc ∫⁻ x, ‖u x‖ₑ ^ p ∂(volume : Measure (ι → ℝ)).map e.symm
      = ∫⁻ y, ‖v y‖ₑ ^ p := by
        refine lintegral_map ?_ e.symm.continuous.measurable
        borelize F
        exact hu.continuous.measurable.nnnorm.coe_nnreal_ennreal.pow_const _
    _ ≤ (∫⁻ y, ‖fderiv ℝ v y‖ₑ) ^ p := lintegral_pow_le_pow_lintegral_fderiv_aux hp hv h2v
    _ = (∫⁻ y, ‖(fderiv ℝ u (e.symm y)).comp (fderiv ℝ e.symm y)‖ₑ) ^ p := by
        congr! with y
        apply fderiv_comp _ (hu.differentiable one_ne_zero _)
        exact e.symm.differentiableAt
    _ ≤ (∫⁻ y, ‖fderiv ℝ u (e.symm y)‖ₑ * ‖(e.symm : (ι → ℝ) →L[ℝ] E)‖ₑ) ^ p := by
        gcongr with y
        rw [e.symm.fderiv]
        apply ContinuousLinearMap.opENorm_comp_le
    _ = (‖(e.symm : (ι → ℝ) →L[ℝ] E)‖ₑ * ∫⁻ y, ‖fderiv ℝ u (e.symm y)‖ₑ) ^ p := by
        rw [lintegral_mul_const, mul_comm]
        fun_prop
    _ = (‖(e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p : ℝ≥0) * (∫⁻ y, ‖fderiv ℝ u (e.symm y)‖ₑ) ^ p := by
        rw [ENNReal.mul_rpow_of_nonneg _ _ h0p, enorm_eq_nnnorm, ← ENNReal.coe_rpow_of_nonneg _ h0p]
    _ = (‖(e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p : ℝ≥0)
        * (∫⁻ x, ‖fderiv ℝ u x‖ₑ ∂(volume : Measure (ι → ℝ)).map e.symm) ^ p := by
        congr
        rw [lintegral_map _ e.symm.continuous.measurable]
        fun_prop