awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
F' : Type u_5
inst_6 : NormedAddCommGroup F'
inst_7 : InnerProductSpace ℝ F'
u : E → F'
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p p' : ℝ≥0
hp_1 : 1 ≤ p
hp'0 : ¬p' = 0
n : ℕ := finrank ℝ E
hn_1 : 0 < n
hp' : (↑p' : ℝ)⁻¹ = (↑p⁻¹ : ℝ) - (↑n : ℝ)⁻¹
n' : ℝ≥0 := NNReal.conjExponent (↑n : ℝ≥0)
h2p : (↑p : ℝ) < (↑n : ℝ)
h0n : 2 ≤ n
hn : NNReal.HolderConjugate (↑n : ℝ≥0) n'
h1n : LE.le (α := ℝ≥0) 1 (↑n : ℝ≥0)
h2n : 0 < HSub.hSub (α := ℝ) (↑n : ℝ) 1
hnp : 0 < (↑n : ℝ) - (↑p : ℝ)
hp : 1 < p
q : ℝ := (↑p : ℝ).conjExponent
hq : (↑p : ℝ).HolderConjugate q
h0p : p ≠ 0
h1p : (↑p : ℝ) ≠ 1
h3p : (↑p : ℝ) - 1 ≠ 0
h2q : 1 / (↑n' : ℝ) - 1 / q = 1 / (↑p' : ℝ)
γ : ℝ≥0 := NNReal.mk ((↑p : ℝ) * HSub.hSub (α := ℝ) (↑n : ℝ) 1 / ((↑n : ℝ) - (↑p : ℝ))) ⋯
h0γ : (↑γ : ℝ) = (↑p : ℝ) * HSub.hSub (α := ℝ) (↑n : ℝ) 1 / ((↑n : ℝ) - (↑p : ℝ))
h1γ : 1 < (↑γ : ℝ)
h2γ : γ * n' = p'
h3γ : ((↑γ : ℝ) - 1) * q = (↑p' : ℝ)
h4γ : (↑γ : ℝ) ≠ 0
h3u : ¬∫⁻ (x : E), ‖u x‖ₑ ^ (↑p' : ℝ) ∂μ = 0
h4u : ∫⁻ (x : E), ‖u x‖ₑ ^ (↑p' : ℝ) ∂μ ≠ ∞
h5u : (∫⁻ (x : E), ‖u x‖ₑ ^ (↑p' : ℝ) ∂μ) ^ (1 / q) ≠ 0
h6u : (∫⁻ (x : E), ‖u x‖ₑ ^ (↑p' : ℝ) ∂μ) ^ (1 / q) ≠ ∞
h7u : Continuous u
v : E → ℝ := fun (x : E) ↦ ‖u x‖ ^ (↑γ : ℝ)
hv : ContDiff ℝ 1 v
h2v : HasCompactSupport v
C : ℝ≥0 := eLpNormLESNormFDerivOneConst μ (↑n' : ℝ)
this :
  (∫⁻ (x : E), ‖u x‖ₑ ^ (↑p' : ℝ) ∂μ) ^ (1 / (↑n' : ℝ)) ≤
    (↑C : ℝ≥0∞) * (↑γ : ℝ≥0∞) * (∫⁻ (x : E), enorm (E := E →L[ℝ] F') (fderiv ℝ u x) ^ (↑p : ℝ) ∂μ) ^ (1 / (↑p : ℝ)) *
      (∫⁻ (x : E), ‖u x‖ₑ ^ (↑p' : ℝ) ∂μ) ^ (1 / q)
⊢ eLpNorm u (↑p' : ℝ≥0∞) μ ≤
    (↑(eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F') (fderiv ℝ u) (↑p : ℝ≥0∞) μ
have eLpNorm : (∫⁻ (x : E), ‖u x‖ₑ ^ (↑p' : ℝ) ∂μ) ^ (1 / (↑p' : ℝ)) ≤
  (↑C : ℝ≥0∞) * (↑γ : ℝ≥0∞) * (∫⁻ (x : E), enorm (E := E →L[ℝ] F') (fderiv ℝ u x) ^ (↑p : ℝ) ∂μ) ^ (1 / (↑p : ℝ))
Tactic: calc
    eLpNorm u p' μ
      = (∫⁻ x, ‖u x‖ₑ ^ (p' : ℝ) ∂μ) ^ (1 / (p' : ℝ)) := eLpNorm_nnreal_eq_lintegral hp'0
    _ ≤ C * γ * (∫⁻ x, ‖fderiv ℝ u x‖ₑ ^ (p : ℝ) ∂μ) ^ (1 / (p : ℝ)) := by
      rwa [← h2q, ENNReal.rpow_sub _ _ h3u h4u, ENNReal.div_le_iff h5u h6u]
    _ = eLpNormLESNormFDerivOfEqInnerConst μ p * eLpNorm (fderiv ℝ u) (↑p) μ := by
      suffices (C : ℝ) * γ = eLpNormLESNormFDerivOfEqInnerConst μ p by
        rw [eLpNorm_nnreal_eq_lintegral h0p]
        congr
        norm_cast at this ⊢
      simp_rw [eLpNormLESNormFDerivOfEqInnerConst, γ]
      refold_let n n' C
      rw [NNReal.coe_mul, NNReal.coe_mk, Real.coe_toNNReal', mul_eq_mul_left_iff, eq_comm,
        max_eq_left_iff]
      left
      positivity
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
F' : Type u_5
inst_6 : NormedAddCommGroup F'
inst_7 : InnerProductSpace ℝ F'
u : E → F'
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p p' : ℝ≥0
hp_1 : 1 ≤ p
hp'0 : ¬p' = 0
n : ℕ := finrank ℝ E
hn_1 : 0 < n
hp' : (↑p' : ℝ)⁻¹ = (↑p⁻¹ : ℝ) - (↑n : ℝ)⁻¹
n' : ℝ≥0 := NNReal.conjExponent (↑n : ℝ≥0)
h2p : (↑p : ℝ) < (↑n : ℝ)
h0n : 2 ≤ n
hn : NNReal.HolderConjugate (↑n : ℝ≥0) n'
h1n : LE.le (α := ℝ≥0) 1 (↑n : ℝ≥0)
h2n : 0 < HSub.hSub (α := ℝ) (↑n : ℝ) 1
hnp : 0 < (↑n : ℝ) - (↑p : ℝ)
hp : 1 < p
q : ℝ := (↑p : ℝ).conjExponent
hq : (↑p : ℝ).HolderConjugate q
h0p : p ≠ 0
h1p : (↑p : ℝ) ≠ 1
h3p : (↑p : ℝ) - 1 ≠ 0
h2q : 1 / (↑n' : ℝ) - 1 / q = 1 / (↑p' : ℝ)
γ : ℝ≥0 := NNReal.mk ((↑p : ℝ) * HSub.hSub (α := ℝ) (↑n : ℝ) 1 / ((↑n : ℝ) - (↑p : ℝ))) ⋯
h0γ : (↑γ : ℝ) = (↑p : ℝ) * HSub.hSub (α := ℝ) (↑n : ℝ) 1 / ((↑n : ℝ) - (↑p : ℝ))
h1γ : 1 < (↑γ : ℝ)
h2γ : γ * n' = p'
h3γ : ((↑γ : ℝ) - 1) * q = (↑p' : ℝ)
h4γ : (↑γ : ℝ) ≠ 0
h3u : ¬∫⁻ (x : E), ‖u x‖ₑ ^ (↑p' : ℝ) ∂μ = 0
h4u : ∫⁻ (x : E), ‖u x‖ₑ ^ (↑p' : ℝ) ∂μ ≠ ∞
h5u : (∫⁻ (x : E), ‖u x‖ₑ ^ (↑p' : ℝ) ∂μ) ^ (1 / q) ≠ 0
h6u : (∫⁻ (x : E), ‖u x‖ₑ ^ (↑p' : ℝ) ∂μ) ^ (1 / q) ≠ ∞
h7u : Continuous u
v : E → ℝ := fun (x : E) ↦ ‖u x‖ ^ (↑γ : ℝ)
hv : ContDiff ℝ 1 v
h2v : HasCompactSupport v
C : ℝ≥0 := eLpNormLESNormFDerivOneConst μ (↑n' : ℝ)
this :
  (∫⁻ (x : E), ‖u x‖ₑ ^ (↑p' : ℝ) ∂μ) ^ (1 / (↑n' : ℝ)) ≤
    (↑C : ℝ≥0∞) * (↑γ : ℝ≥0∞) * (∫⁻ (x : E), enorm (E := E →L[ℝ] F') (fderiv ℝ u x) ^ (↑p : ℝ) ∂μ) ^ (1 / (↑p : ℝ)) *
      (∫⁻ (x : E), ‖u x‖ₑ ^ (↑p' : ℝ) ∂μ) ^ (1 / q)
eLpNorm :
  (∫⁻ (x : E), ‖u x‖ₑ ^ (↑p' : ℝ) ∂μ) ^ (1 / (↑p' : ℝ)) ≤
    (↑C : ℝ≥0∞) * (↑γ : ℝ≥0∞) * (∫⁻ (x : E), enorm (E := E →L[ℝ] F') (fderiv ℝ u x) ^ (↑p : ℝ) ∂μ) ^ (1 / (↑p : ℝ))
⊢ MeasureTheory.eLpNorm u (↑p' : ℝ≥0∞) μ ≤
    (↑(eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)) : ℝ≥0∞) *
      MeasureTheory.eLpNorm (ε := E →L[ℝ] F') (fderiv ℝ u) (↑p : ℝ≥0∞) μ
have eLpNorm₁ : (↑C : ℝ≥0∞) * (↑γ : ℝ≥0∞) * (∫⁻ (x : E), enorm (E := E →L[ℝ] F') (fderiv ℝ u x) ^ (↑p : ℝ) ∂μ) ^ (1 / (↑p : ℝ)) =
  (↑(eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)) : ℝ≥0∞) *
    MeasureTheory.eLpNorm (ε := E →L[ℝ] F') (fderiv ℝ u) (↑p : ℝ≥0∞) μ
Tactic: calc
    eLpNorm u p' μ
      = (∫⁻ x, ‖u x‖ₑ ^ (p' : ℝ) ∂μ) ^ (1 / (p' : ℝ)) := eLpNorm_nnreal_eq_lintegral hp'0
    _ ≤ C * γ * (∫⁻ x, ‖fderiv ℝ u x‖ₑ ^ (p : ℝ) ∂μ) ^ (1 / (p : ℝ)) := by
      rwa [← h2q, ENNReal.rpow_sub _ _ h3u h4u, ENNReal.div_le_iff h5u h6u]
    _ = eLpNormLESNormFDerivOfEqInnerConst μ p * eLpNorm (fderiv ℝ u) (↑p) μ := by
      suffices (C : ℝ) * γ = eLpNormLESNormFDerivOfEqInnerConst μ p by
        rw [eLpNorm_nnreal_eq_lintegral h0p]
        congr
        norm_cast at this ⊢
      simp_rw [eLpNormLESNormFDerivOfEqInnerConst, γ]
      refold_let n n' C
      rw [NNReal.coe_mul, NNReal.coe_mk, Real.coe_toNNReal', mul_eq_mul_left_iff, eq_comm,
        max_eq_left_iff]
      left
      positivity
-- 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
inst_8 : FiniteDimensional ℝ F
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p p' : ℝ≥0
hp : 1 ≤ p
hn : 0 < finrank ℝ E
hp' : (↑p' : ℝ)⁻¹ = (↑p⁻¹ : ℝ) - (↑(finrank ℝ E) : ℝ)⁻¹
F' : Type := EuclideanSpace ℝ (Fin (finrank ℝ F))
e : F ≃L[ℝ] F' := toEuclidean
C₁ : ℝ≥0 := ‖(↑e.symm : F' →L[ℝ] F)‖₊
C : ℝ≥0 := eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)
C₂ : ℝ≥0 := ‖(↑e : F →L[ℝ] F')‖₊
v : E → F' := (⇑e : (a : F) → F') ∘ u
⊢ eLpNorm u (↑p' : ℝ≥0∞) μ ≤
    (↑(SNormLESNormFDerivOfEqConst F μ (↑p : ℝ)) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F) (fderiv ℝ u) (↑p : ℝ≥0∞) μ
have hv : ContDiff ℝ 1 v
Tactic: have hv : ContDiff ℝ 1 v := e.contDiff.comp hu
-- 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
inst_8 : FiniteDimensional ℝ F
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p p' : ℝ≥0
hp : 1 ≤ p
hn : 0 < finrank ℝ E
hp' : (↑p' : ℝ)⁻¹ = (↑p⁻¹ : ℝ) - (↑(finrank ℝ E) : ℝ)⁻¹
F' : Type := EuclideanSpace ℝ (Fin (finrank ℝ F))
e : F ≃L[ℝ] F' := toEuclidean
C₁ : ℝ≥0 := ‖(↑e.symm : F' →L[ℝ] F)‖₊
C : ℝ≥0 := eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)
C₂ : ℝ≥0 := ‖(↑e : F →L[ℝ] F')‖₊
v : E → F' := (⇑e : (a : F) → F') ∘ u
hv : ContDiff ℝ 1 v
⊢ eLpNorm u (↑p' : ℝ≥0∞) μ ≤
    (↑(SNormLESNormFDerivOfEqConst F μ (↑p : ℝ)) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F) (fderiv ℝ u) (↑p : ℝ≥0∞) μ
have h2v : HasCompactSupport v
Tactic: have h2v : HasCompactSupport v := h2u.comp_left e.map_zero
-- 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
inst_8 : FiniteDimensional ℝ F
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p p' : ℝ≥0
hp : 1 ≤ p
hn : 0 < finrank ℝ E
hp' : (↑p' : ℝ)⁻¹ = (↑p⁻¹ : ℝ) - (↑(finrank ℝ E) : ℝ)⁻¹
F' : Type := EuclideanSpace ℝ (Fin (finrank ℝ F))
e : F ≃L[ℝ] F' := toEuclidean
C₁ : ℝ≥0 := ‖(↑e.symm : F' →L[ℝ] F)‖₊
C : ℝ≥0 := eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)
C₂ : ℝ≥0 := ‖(↑e : F →L[ℝ] F')‖₊
v : E → F' := (⇑e : (a : F) → F') ∘ u
hv : ContDiff ℝ 1 v
h2v : HasCompactSupport v
⊢ eLpNorm u (↑p' : ℝ≥0∞) μ ≤
    (↑(SNormLESNormFDerivOfEqConst F μ (↑p : ℝ)) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F) (fderiv ℝ u) (↑p : ℝ≥0∞) μ
have this : eLpNorm v (↑p' : ℝ≥0∞) μ ≤
  (↑(eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F') (fderiv ℝ v) (↑p : ℝ≥0∞) μ
Tactic: have := eLpNorm_le_eLpNorm_fderiv_of_eq_inner μ hv h2v hp hn hp'
-- 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
inst_8 : FiniteDimensional ℝ F
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p p' : ℝ≥0
hp : 1 ≤ p
hn : 0 < finrank ℝ E
hp' : (↑p' : ℝ)⁻¹ = (↑p⁻¹ : ℝ) - (↑(finrank ℝ E) : ℝ)⁻¹
F' : Type := EuclideanSpace ℝ (Fin (finrank ℝ F))
e : F ≃L[ℝ] F' := toEuclidean
C₁ : ℝ≥0 := ‖(↑e.symm : F' →L[ℝ] F)‖₊
C : ℝ≥0 := eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)
C₂ : ℝ≥0 := ‖(↑e : F →L[ℝ] F')‖₊
v : E → F' := (⇑e : (a : F) → F') ∘ u
hv : ContDiff ℝ 1 v
h2v : HasCompactSupport v
this :
  eLpNorm v (↑p' : ℝ≥0∞) μ ≤
    (↑(eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F') (fderiv ℝ v) (↑p : ℝ≥0∞) μ
x : E
⊢ norm (E := E →L[ℝ] F') (fderiv ℝ v x) = norm (E := E →L[ℝ] F') (fderiv ℝ (⇑e : (a : F) → F') (u x) ∘SL fderiv ℝ u x)
have rw : norm (E := E →L[ℝ] F') (fderiv ℝ (⇑e : (a : F) → F') (u x) ∘SL fderiv ℝ u x) =
  norm (E := E →L[ℝ] F') (fderiv ℝ (⇑e : (a : F) → F') (u x) ∘SL fderiv ℝ u x)
Tactic: rw [fderiv_comp x e.differentiableAt (hu.differentiable one_ne_zero x)]
-- 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
inst_8 : FiniteDimensional ℝ F
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p p' : ℝ≥0
hp : 1 ≤ p
hn : 0 < finrank ℝ E
hp' : (↑p' : ℝ)⁻¹ = (↑p⁻¹ : ℝ) - (↑(finrank ℝ E) : ℝ)⁻¹
F' : Type := EuclideanSpace ℝ (Fin (finrank ℝ F))
e : F ≃L[ℝ] F' := toEuclidean
C₁ : ℝ≥0 := ‖(↑e.symm : F' →L[ℝ] F)‖₊
C : ℝ≥0 := eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)
C₂ : ℝ≥0 := ‖(↑e : F →L[ℝ] F')‖₊
v : E → F' := (⇑e : (a : F) → F') ∘ u
hv : ContDiff ℝ 1 v
h2v : HasCompactSupport v
this :
  eLpNorm v (↑p' : ℝ≥0∞) μ ≤
    (↑(eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F') (fderiv ℝ v) (↑p : ℝ≥0∞) μ
x : E
⊢ norm (E := F →L[ℝ] F') (fderiv ℝ (⇑e : (a : F) → F') (u x)) * norm (E := E →L[ℝ] F) (fderiv ℝ u x) =
    (↑C₂ : ℝ) * norm (E := E →L[ℝ] F) (fderiv ℝ u x)
have simp_rw : ‖(↑e : F →L[ℝ] F')‖ * norm (E := E →L[ℝ] F) (fderiv ℝ u x) = (↑C₂ : ℝ) * norm (E := E →L[ℝ] F) (fderiv ℝ u x)
Tactic: simp_rw [e.fderiv, C₂, coe_nnnorm]
-- 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
inst_8 : FiniteDimensional ℝ F
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p p' : ℝ≥0
hp : 1 ≤ p
hn : 0 < finrank ℝ E
hp' : (↑p' : ℝ)⁻¹ = (↑p⁻¹ : ℝ) - (↑(finrank ℝ E) : ℝ)⁻¹
F' : Type := EuclideanSpace ℝ (Fin (finrank ℝ F))
e : F ≃L[ℝ] F' := toEuclidean
C₁ : ℝ≥0 := ‖(↑e.symm : F' →L[ℝ] F)‖₊
C : ℝ≥0 := eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)
C₂ : ℝ≥0 := ‖(↑e : F →L[ℝ] F')‖₊
v : E → F' := (⇑e : (a : F) → F') ∘ u
hv : ContDiff ℝ 1 v
h2v : HasCompactSupport v
this :
  eLpNorm v (↑p' : ℝ≥0∞) μ ≤
    (↑(eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F') (fderiv ℝ v) (↑p : ℝ≥0∞) μ
⊢ eLpNorm u (↑p' : ℝ≥0∞) μ ≤
    (↑(SNormLESNormFDerivOfEqConst F μ (↑p : ℝ)) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F) (fderiv ℝ u) (↑p : ℝ≥0∞) μ
have h4v : ∀ (x : E), norm (E := E →L[ℝ] F') (fderiv ℝ v x) ≤ (↑C₂ : ℝ) * norm (E := E →L[ℝ] F) (fderiv ℝ u x)
Tactic: have h4v : ∀ x, ‖fderiv ℝ v x‖ ≤ C₂ * ‖fderiv ℝ u x‖ := fun x ↦ calc
    ‖fderiv ℝ v x‖
      = ‖(fderiv ℝ e (u x)).comp (fderiv ℝ u x)‖ := by
      rw [fderiv_comp x e.differentiableAt (hu.differentiable one_ne_zero x)]
    _ ≤ ‖fderiv ℝ e (u x)‖ * ‖fderiv ℝ u x‖ :=
      (fderiv ℝ e (u x)).opNorm_comp_le (fderiv ℝ u x)
    _ = C₂ * ‖fderiv ℝ u x‖ := by simp_rw [e.fderiv, C₂, coe_nnnorm]
-- 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
inst_8 : FiniteDimensional ℝ F
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p p' : ℝ≥0
hp : 1 ≤ p
hn : 0 < finrank ℝ E
hp' : (↑p' : ℝ)⁻¹ = (↑p⁻¹ : ℝ) - (↑(finrank ℝ E) : ℝ)⁻¹
F' : Type := EuclideanSpace ℝ (Fin (finrank ℝ F))
e : F ≃L[ℝ] F' := toEuclidean
C₁ : ℝ≥0 := ‖(↑e.symm : F' →L[ℝ] F)‖₊
C : ℝ≥0 := eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)
C₂ : ℝ≥0 := ‖(↑e : F →L[ℝ] F')‖₊
v : E → F' := (⇑e : (a : F) → F') ∘ u
hv : ContDiff ℝ 1 v
h2v : HasCompactSupport v
this :
  eLpNorm v (↑p' : ℝ≥0∞) μ ≤
    (↑(eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F') (fderiv ℝ v) (↑p : ℝ≥0∞) μ
h4v : ∀ (x : E), norm (E := E →L[ℝ] F') (fderiv ℝ v x) ≤ (↑C₂ : ℝ) * norm (E := E →L[ℝ] F) (fderiv ℝ u x)
simp_rw :
  eLpNorm u (↑p' : ℝ≥0∞) μ =
    eLpNorm (ε := F) (comp (β := F') (⇑e.symm : (a : F') → F) ((⇑e : (a : F) → F') ∘ u)) (↑p' : ℝ≥0∞) μ
⊢ eLpNorm u (↑p' : ℝ≥0∞) μ = eLpNorm (ε := F) ((⇑e.symm : (a : F') → F) ∘ v) (↑p' : ℝ≥0∞) μ
have simp_rw₁ : eLpNorm u (↑p' : ℝ≥0∞) μ =
  eLpNorm.{u_4, u_3} (ε := F) (fun (x : E) ↦ (e.symm : (a : F') → F) ((e : (a : F) → F') (u x) : F')) (↑p' : ℝ≥0∞) μ
Tactic: simp_rw [v, Function.comp_def, e.symm_apply_apply]
-- 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
inst_8 : FiniteDimensional ℝ F
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p p' : ℝ≥0
hp : 1 ≤ p
hn : 0 < finrank ℝ E
hp' : (↑p' : ℝ)⁻¹ = (↑p⁻¹ : ℝ) - (↑(finrank ℝ E) : ℝ)⁻¹
F' : Type := EuclideanSpace ℝ (Fin (finrank ℝ F))
e : F ≃L[ℝ] F' := toEuclidean
C₁ : ℝ≥0 := ‖(↑e.symm : F' →L[ℝ] F)‖₊
C : ℝ≥0 := eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)
C₂ : ℝ≥0 := ‖(↑e : F →L[ℝ] F')‖₊
v : E → F' := (⇑e : (a : F) → F') ∘ u
hv : ContDiff ℝ 1 v
h2v : HasCompactSupport v
this :
  eLpNorm v (↑p' : ℝ≥0∞) μ ≤
    (↑(eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F') (fderiv ℝ v) (↑p : ℝ≥0∞) μ
h4v : ∀ (x : E), norm (E := E →L[ℝ] F') (fderiv ℝ v x) ≤ (↑C₂ : ℝ) * norm (E := E →L[ℝ] F) (fderiv ℝ u x)
⊢ eLpNorm (ε := F) ((⇑e.symm : (a : F') → F) ∘ v) (↑p' : ℝ≥0∞) μ ≤ C₁ • eLpNorm v (↑p' : ℝ≥0∞) μ
have h : ∀ᵐ (x : E) ∂μ, nnnorm (E := F) (((⇑e.symm : (a : F') → F) ∘ v) x) ≤ C₁ * ‖v x‖₊
Tactic: apply eLpNorm_le_nnreal_smul_eLpNorm_of_ae_le_mul
-- 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
inst_8 : FiniteDimensional ℝ F
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p p' : ℝ≥0
hp : 1 ≤ p
hn : 0 < finrank ℝ E
hp' : (↑p' : ℝ)⁻¹ = (↑p⁻¹ : ℝ) - (↑(finrank ℝ E) : ℝ)⁻¹
F' : Type := EuclideanSpace ℝ (Fin (finrank ℝ F))
e : F ≃L[ℝ] F' := toEuclidean
C₁ : ℝ≥0 := ‖(↑e.symm : F' →L[ℝ] F)‖₊
C : ℝ≥0 := eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)
C₂ : ℝ≥0 := ‖(↑e : F →L[ℝ] F')‖₊
v : E → F' := (⇑e : (a : F) → F') ∘ u
hv : ContDiff ℝ 1 v
h2v : HasCompactSupport v
this :
  eLpNorm v (↑p' : ℝ≥0∞) μ ≤
    (↑(eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F') (fderiv ℝ v) (↑p : ℝ≥0∞) μ
h4v : ∀ (x : E), norm (E := E →L[ℝ] F') (fderiv ℝ v x) ≤ (↑C₂ : ℝ) * norm (E := E →L[ℝ] F) (fderiv ℝ u x)
⊢ (↑C₁ : ℝ≥0∞) * eLpNorm v (↑p' : ℝ≥0∞) μ ≤
    (↑C₁ : ℝ≥0∞) * (↑C : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F') (fderiv ℝ v) (↑p : ℝ≥0∞) μ
have rw : (↑C₁ : ℝ≥0∞) * eLpNorm v (↑p' : ℝ≥0∞) μ ≤
  (↑C₁ : ℝ≥0∞) * ((↑C : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F') (fderiv ℝ v) (↑p : ℝ≥0∞) μ)
Tactic: rw [mul_assoc]
-- 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
inst_8 : FiniteDimensional ℝ F
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p p' : ℝ≥0
hp : 1 ≤ p
hn : 0 < finrank ℝ E
hp' : (↑p' : ℝ)⁻¹ = (↑p⁻¹ : ℝ) - (↑(finrank ℝ E) : ℝ)⁻¹
F' : Type := EuclideanSpace ℝ (Fin (finrank ℝ F))
e : F ≃L[ℝ] F' := toEuclidean
C₁ : ℝ≥0 := ‖(↑e.symm : F' →L[ℝ] F)‖₊
C : ℝ≥0 := eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)
C₂ : ℝ≥0 := ‖(↑e : F →L[ℝ] F')‖₊
v : E → F' := (⇑e : (a : F) → F') ∘ u
hv : ContDiff ℝ 1 v
h2v : HasCompactSupport v
this :
  eLpNorm v (↑p' : ℝ≥0∞) μ ≤
    (↑(eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F') (fderiv ℝ v) (↑p : ℝ≥0∞) μ
h4v : ∀ (x : E), norm (E := E →L[ℝ] F') (fderiv ℝ v x) ≤ (↑C₂ : ℝ) * norm (E := E →L[ℝ] F) (fderiv ℝ u x)
⊢ (↑C₁ : ℝ≥0∞) * (↑C : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F') (fderiv ℝ v) (↑p : ℝ≥0∞) μ ≤
    (↑C₁ : ℝ≥0∞) * (↑C : ℝ≥0∞) * ((↑C₂ : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F) (fderiv ℝ u) (↑p : ℝ≥0∞) μ)
have bc : eLpNorm (ε := E →L[ℝ] F') (fderiv ℝ v) (↑p : ℝ≥0∞) μ ≤
  (↑C₂ : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F) (fderiv ℝ u) (↑p : ℝ≥0∞) μ
Tactic: gcongr
-- 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
inst_8 : FiniteDimensional ℝ F
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p p' : ℝ≥0
hp : 1 ≤ p
hn : 0 < finrank ℝ E
hp' : (↑p' : ℝ)⁻¹ = (↑p⁻¹ : ℝ) - (↑(finrank ℝ E) : ℝ)⁻¹
F' : Type := EuclideanSpace ℝ (Fin (finrank ℝ F))
e : F ≃L[ℝ] F' := toEuclidean
C₁ : ℝ≥0 := ‖(↑e.symm : F' →L[ℝ] F)‖₊
C : ℝ≥0 := eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)
C₂ : ℝ≥0 := ‖(↑e : F →L[ℝ] F')‖₊
v : E → F' := (⇑e : (a : F) → F') ∘ u
hv : ContDiff ℝ 1 v
h2v : HasCompactSupport v
this :
  eLpNorm v (↑p' : ℝ≥0∞) μ ≤
    (↑(eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F') (fderiv ℝ v) (↑p : ℝ≥0∞) μ
h4v : ∀ (x : E), norm (E := E →L[ℝ] F') (fderiv ℝ v x) ≤ (↑C₂ : ℝ) * norm (E := E →L[ℝ] F) (fderiv ℝ u x)
⊢ (↑C₁ : ℝ≥0∞) * (↑C : ℝ≥0∞) * ((↑C₂ : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F) (fderiv ℝ u) (↑p : ℝ≥0∞) μ) =
    (↑(SNormLESNormFDerivOfEqConst F μ (↑p : ℝ)) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F) (fderiv ℝ u) (↑p : ℝ≥0∞) μ
have simp_rw : (↑(nnnorm.{u_3} (E := F' →L[ℝ] F) (↑(ContinuousLinearEquiv.symm toEuclidean) : F' →L[ℝ] F)) : ℝ≥0∞) *
      (↑(eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)) : ℝ≥0∞) *
    ((↑(nnnorm.{u_3} (E := F →L[ℝ] F') (↑toEuclidean : F →L[ℝ] F')) : ℝ≥0∞) *
      eLpNorm (ε := E →L[ℝ] F) (fderiv ℝ u) (↑p : ℝ≥0∞) μ) =
  (↑(nnnorm.{u_3} (E := EuclideanSpace ℝ (Fin (finrank ℝ F)) →L[ℝ] F)
              (↑(ContinuousLinearEquiv.symm toEuclidean) : EuclideanSpace ℝ (Fin (finrank ℝ F)) →L[ℝ] F) *
            eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ) *
          nnnorm.{u_3} (E := F →L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ F)))
            (↑toEuclidean : F →L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ F)))) :
      ℝ≥0∞) *
    eLpNorm (ε := E →L[ℝ] F) (fderiv ℝ u) (↑p : ℝ≥0∞) μ
Tactic: simp_rw [C₂, C₁, C, e, SNormLESNormFDerivOfEqConst]
-- 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
inst_8 : FiniteDimensional ℝ F
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p p' : ℝ≥0
hp : 1 ≤ p
hn : 0 < finrank ℝ E
hp' : (↑p' : ℝ)⁻¹ = (↑p⁻¹ : ℝ) - (↑(finrank ℝ E) : ℝ)⁻¹
F' : Type := EuclideanSpace ℝ (Fin (finrank ℝ F))
e : F ≃L[ℝ] F' := toEuclidean
C₁ : ℝ≥0 := ‖(↑e.symm : F' →L[ℝ] F)‖₊
C : ℝ≥0 := eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)
C₂ : ℝ≥0 := ‖(↑e : F →L[ℝ] F')‖₊
v : E → F' := (⇑e : (a : F) → F') ∘ u
hv : ContDiff ℝ 1 v
h2v : HasCompactSupport v
this :
  eLpNorm v (↑p' : ℝ≥0∞) μ ≤
    (↑(eLpNormLESNormFDerivOfEqInnerConst μ (↑p : ℝ)) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F') (fderiv ℝ v) (↑p : ℝ≥0∞) μ
h4v : ∀ (x : E), norm (E := E →L[ℝ] F') (fderiv ℝ v x) ≤ (↑C₂ : ℝ) * norm (E := E →L[ℝ] F) (fderiv ℝ u x)
⊢ eLpNorm u (↑p' : ℝ≥0∞) μ ≤
    (↑(SNormLESNormFDerivOfEqConst F μ (↑p : ℝ)) : ℝ≥0∞) * eLpNorm (ε := E →L[ℝ] F) (fderiv ℝ u) (↑p : ℝ≥0∞) μ
have calc : eLpNorm u (↑p' : ℝ≥0∞) μ = eLpNorm (ε := F) ((⇑e.symm : (a : F') → F) ∘ v) (↑p' : ℝ≥0∞) μ
Tactic: calc eLpNorm u p' μ
      = eLpNorm (e.symm ∘ v) p' μ := by simp_rw [v, Function.comp_def, e.symm_apply_apply]
    _ ≤ C₁ • eLpNorm v p' μ := by
      apply eLpNorm_le_nnreal_smul_eLpNorm_of_ae_le_mul
      exact Eventually.of_forall (fun x ↦ (e.symm : F' →L[ℝ] F).le_opNNNorm _)
    _ = C₁ * eLpNorm v p' μ := rfl
    _ ≤ C₁ * C * eLpNorm (fderiv ℝ v) p μ := by rw [mul_assoc]; gcongr
    _ ≤ C₁ * C * (C₂ * eLpNorm (fderiv ℝ u) p μ) := by
      gcongr; exact eLpNorm_le_nnreal_smul_eLpNorm_of_ae_le_mul (Eventually.of_forall h4v) p
    _ = SNormLESNormFDerivOfEqConst F μ p * eLpNorm (fderiv ℝ u) p μ := by
      simp_rw [C₂, C₁, C, e, SNormLESNormFDerivOfEqConst]
      push_cast
      simp_rw [mul_assoc]