awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
ι : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Fintype ι
p : ℝ
hp : Real.HolderConjugate (↑#ι : ℝ) p
u : (ι → ℝ) → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
this : 1 ≤ HSub.hSub (α := ℝ) (↑#ι : ℝ) 1
⊢ ∫⁻ (x : ι → ℝ), ∏ _i : ι, ‖u x‖ₑ ^ (1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1) ≤
    ∫⁻ (x : (a : ι) → ℝ),
      ∏ i : ι,
        (∫⁻ (xᵢ : ℝ),
            enorm (E := ContinuousLinearMap.{0, 0, u_1, u_3} (RingHom.id ℝ) (ι → ℝ) F)
              (fderiv ℝ u (update (β := fun (a : ι) ↦ ℝ) x i xᵢ))) ^
          (1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1)
have hfg : ∀ (x : ι → ℝ) (i : ι),
  Membership.mem (γ := Finset ι) Finset.univ i →
    ‖u x‖ₑ ≤
      ∫⁻ (xᵢ : ℝ),
        enorm (E := ContinuousLinearMap.{0, 0, u_1, u_3} (RingHom.id ℝ) (ι → ℝ) F)
          (fderiv ℝ u (update (β := fun (a : ι) ↦ ℝ) x i xᵢ))
Tactic: gcongr with x i
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
ι : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Fintype ι
p : ℝ
hp : Real.HolderConjugate (↑#ι : ℝ) p
u : (ι → ℝ) → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
this : 1 ≤ HSub.hSub (α := ℝ) (↑#ι : ℝ) 1
x : ι → ℝ
i : ι
h : Membership.mem (γ := Finset ι) Finset.univ i
⊢ ‖u x‖ₑ ≤ ∫⁻ (xᵢ : ℝ) in Set.Iic (x i), ‖deriv (u ∘ update (β := fun (a : ι) ↦ ℝ) x i) xᵢ‖ₑ
have apply : ContDiff ℝ 1 (u ∘ update (β := fun (a : ι) ↦ ℝ) x i)
Tactic: apply le_trans (by simp) (HasCompactSupport.enorm_le_lintegral_Ici_deriv _ _ _)
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
ι : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Fintype ι
p : ℝ
hp : Real.HolderConjugate (↑#ι : ℝ) p
u : (ι → ℝ) → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
this : 1 ≤ HSub.hSub (α := ℝ) (↑#ι : ℝ) 1
x : ι → ℝ
i : ι
h : Membership.mem (γ := Finset ι) Finset.univ i
apply : ContDiff ℝ 1 (u ∘ update (β := fun (a : ι) ↦ ℝ) x i)
⊢ ‖u x‖ₑ ≤ ∫⁻ (xᵢ : ℝ) in Set.Iic (x i), ‖deriv (u ∘ update (β := fun (a : ι) ↦ ℝ) x i) xᵢ‖ₑ
have apply₁ : HasCompactSupport (u ∘ update (β := fun (a : ι) ↦ ℝ) x i)
Tactic: apply le_trans (by simp) (HasCompactSupport.enorm_le_lintegral_Ici_deriv _ _ _)
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
ι : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Fintype ι
p : ℝ
hp : Real.HolderConjugate (↑#ι : ℝ) p
u : (ι → ℝ) → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
this : 1 ≤ HSub.hSub (α := ℝ) (↑#ι : ℝ) 1
x : ι → ℝ
i : ι
h : Membership.mem (γ := Finset ι) Finset.univ i
⊢ ‖u x‖ₑ ≤
    ∫⁻ (xᵢ : ℝ),
      enorm (E := ContinuousLinearMap.{0, 0, u_1, u_3} (RingHom.id ℝ) (ι → ℝ) F)
        (fderiv ℝ u (update (β := fun (a : ι) ↦ ℝ) x i xᵢ))
have hfg : ∫⁻ (xᵢ : ℝ) in Set.Iic (x i), ‖deriv (u ∘ update (β := fun (a : ι) ↦ ℝ) x i) xᵢ‖ₑ ≤
  ∫⁻ (xᵢ : ℝ),
    enorm (E := ContinuousLinearMap.{0, 0, u_1, u_3} (RingHom.id ℝ) (ι → ℝ) F)
      (fderiv ℝ u (update (β := fun (a : ι) ↦ ℝ) x i xᵢ))
Tactic: calc ‖u x‖ₑ
    _ ≤ ∫⁻ xᵢ in Iic (x i), ‖deriv (u ∘ update x i) xᵢ‖ₑ := by
        apply le_trans (by simp) (HasCompactSupport.enorm_le_lintegral_Ici_deriv _ _ _)
        · exact hu.comp (by convert! contDiff_update 1 x i)
        · exact h2u.comp_isClosedEmbedding (isClosedEmbedding_update x i)
    _ ≤ ∫⁻ xᵢ, ‖fderiv ℝ u (update x i xᵢ)‖ₑ := ?_
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
ι : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Fintype ι
p : ℝ
hp : Real.HolderConjugate (↑#ι : ℝ) p
u : (ι → ℝ) → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
this : 1 ≤ HSub.hSub (α := ℝ) (↑#ι : ℝ) 1
x : ι → ℝ
i : ι
h : Membership.mem (γ := Finset ι) Finset.univ i
⊢ ∫⁻ (xᵢ : ℝ) in Set.Iic (x i), ‖deriv (u ∘ update (β := fun (a : ι) ↦ ℝ) x i) xᵢ‖ₑ ≤
    ∫⁻ (xᵢ : ℝ),
      enorm (E := ContinuousLinearMap.{0, 0, u_1, u_3} (RingHom.id ℝ) (ι → ℝ) F)
        (fderiv ℝ u (update (β := fun (a : ι) ↦ ℝ) x i xᵢ))
have hfg : Measure.restrict volume (Set.Iic (x i)) ≤ volume
Tactic: gcongr with y
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
ι : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Fintype ι
p : ℝ
hp : Real.HolderConjugate (↑#ι : ℝ) p
u : (ι → ℝ) → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
this : 1 ≤ HSub.hSub (α := ℝ) (↑#ι : ℝ) 1
x : ι → ℝ
i : ι
h : Membership.mem (γ := Finset ι) Finset.univ i
hfg : Measure.restrict volume (Set.Iic (x i)) ≤ volume
⊢ ∫⁻ (xᵢ : ℝ) in Set.Iic (x i), ‖deriv (u ∘ update (β := fun (a : ι) ↦ ℝ) x i) xᵢ‖ₑ ≤
    ∫⁻ (xᵢ : ℝ),
      enorm (E := ContinuousLinearMap.{0, 0, u_1, u_3} (RingHom.id ℝ) (ι → ℝ) F)
        (fderiv ℝ u (update (β := fun (a : ι) ↦ ℝ) x i xᵢ))
have hfg₁ : ∀ (y : ℝ),
  ‖deriv (u ∘ update (β := fun (a : ι) ↦ ℝ) x i) y‖ₑ ≤
    enorm (E := ContinuousLinearMap.{0, 0, u_1, u_3} (RingHom.id ℝ) (ι → ℝ) F)
      (fderiv ℝ u (update (β := fun (a : ι) ↦ ℝ) x i y))
Tactic: gcongr with y
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
ι : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Fintype ι
p : ℝ
hp : Real.HolderConjugate (↑#ι : ℝ) p
u : (ι → ℝ) → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
this : 1 ≤ HSub.hSub (α := ℝ) (↑#ι : ℝ) 1
x : ι → ℝ
i : ι
h : Membership.mem (γ := Finset ι) Finset.univ i
y : ℝ
⊢ ‖deriv (u ∘ update (β := fun (a : ι) ↦ ℝ) x i) y‖ₑ =
    enorm.{u_3} (E := F)
      ((fderiv ℝ u (update (β := fun (a : ι) ↦ ℝ) x i y) : (a : ι → ℝ) → F)
          (deriv (update (β := fun (a : ι) ↦ ℝ) x i) y) :
        F)
have rw : enorm.{u_3} (E := F)
    ((fderiv ℝ u (update (β := fun (a : ι) ↦ ℝ) x i y) : (a : ι → ℝ) → F)
        (deriv (update (β := fun (a : ι) ↦ ℝ) x i) y) :
      F) =
  enorm.{u_3} (E := F)
    ((fderiv ℝ u (update (β := fun (a : ι) ↦ ℝ) x i y) : (a : ι → ℝ) → F)
        (deriv (update (β := fun (a : ι) ↦ ℝ) x i) y) :
      F)
Tactic: rw [fderiv_comp_deriv _ (hu.differentiable one_ne_zero).differentiableAt
          (hasDerivAt_update x i y).differentiableAt]
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
ι : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Fintype ι
p : ℝ
hp : Real.HolderConjugate (↑#ι : ℝ) p
u : (ι → ℝ) → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
this : 1 ≤ HSub.hSub (α := ℝ) (↑#ι : ℝ) 1
x : ι → ℝ
i : ι
h : Membership.mem (γ := Finset ι) Finset.univ i
y : ℝ
⊢ ‖deriv (u ∘ update (β := fun (a : ι) ↦ ℝ) x i) y‖ₑ ≤
    enorm (E := ContinuousLinearMap.{0, 0, u_1, u_3} (RingHom.id ℝ) (ι → ℝ) F)
      (fderiv ℝ u (update (β := fun (a : ι) ↦ ℝ) x i y))
have calc : ‖deriv (u ∘ update (β := fun (a : ι) ↦ ℝ) x i) y‖ₑ =
  enorm.{u_3} (E := F)
    ((fderiv ℝ u (update (β := fun (a : ι) ↦ ℝ) x i y) : (a : ι → ℝ) → F)
        (deriv (update (β := fun (a : ι) ↦ ℝ) x i) y) :
      F)
Tactic: calc ‖deriv (u ∘ update x i) y‖ₑ = ‖fderiv ℝ u (update x i y) (deriv (update x i) y)‖ₑ := by
        rw [fderiv_comp_deriv _ (hu.differentiable one_ne_zero).differentiableAt
          (hasDerivAt_update x i y).differentiableAt]
    _ ≤ ‖fderiv ℝ u (update x i y)‖ₑ * ‖deriv (update x i) y‖ₑ := ContinuousLinearMap.le_opENorm _ _
    _ ≤ ‖fderiv ℝ u (update x i y)‖ₑ := by simp [deriv_update, Pi.enorm_single]
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
ι : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Fintype ι
p : ℝ
hp : Real.HolderConjugate (↑#ι : ℝ) p
u : (ι → ℝ) → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
this : 1 ≤ HSub.hSub (α := ℝ) (↑#ι : ℝ) 1
x : ι → ℝ
i : ι
h : Membership.mem (γ := Finset ι) Finset.univ i
y : ℝ
calc :
  ‖deriv (u ∘ update (β := fun (a : ι) ↦ ℝ) x i) y‖ₑ =
    enorm.{u_3} (E := F)
      ((fderiv ℝ u (update (β := fun (a : ι) ↦ ℝ) x i y) : (a : ι → ℝ) → F)
          (deriv (update (β := fun (a : ι) ↦ ℝ) x i) y) :
        F)
⊢ ‖deriv (u ∘ update (β := fun (a : ι) ↦ ℝ) x i) y‖ₑ ≤
    enorm (E := ContinuousLinearMap.{0, 0, u_1, u_3} (RingHom.id ℝ) (ι → ℝ) F)
      (fderiv ℝ u (update (β := fun (a : ι) ↦ ℝ) x i y))
have calc₁ : enorm (E := ContinuousLinearMap.{0, 0, u_1, u_3} (RingHom.id ℝ) (ι → ℝ) F)
      (fderiv ℝ u (update (β := fun (a : ι) ↦ ℝ) x i y)) *
    ‖deriv (update (β := fun (a : ι) ↦ ℝ) x i) y‖ₑ ≤
  enorm (E := ContinuousLinearMap.{0, 0, u_1, u_3} (RingHom.id ℝ) (ι → ℝ) F)
    (fderiv ℝ u (update (β := fun (a : ι) ↦ ℝ) x i y))
Tactic: calc ‖deriv (u ∘ update x i) y‖ₑ = ‖fderiv ℝ u (update x i y) (deriv (update x i) y)‖ₑ := by
        rw [fderiv_comp_deriv _ (hu.differentiable one_ne_zero).differentiableAt
          (hasDerivAt_update x i y).differentiableAt]
    _ ≤ ‖fderiv ℝ u (update x i y)‖ₑ * ‖deriv (update x i) y‖ₑ := ContinuousLinearMap.le_opENorm _ _
    _ ≤ ‖fderiv ℝ u (update x i y)‖ₑ := by simp [deriv_update, Pi.enorm_single]
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
ι : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Fintype ι
p : ℝ
hp : Real.HolderConjugate (↑#ι : ℝ) p
u : (ι → ℝ) → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
⊢ ∫⁻ (x : ι → ℝ), ‖u x‖ₑ ^ p ≤
    (∫⁻ (x : ι → ℝ), enorm (E := ContinuousLinearMap.{0, 0, u_1, u_3} (RingHom.id ℝ) (ι → ℝ) F) (fderiv ℝ u x)) ^ p
have For : 1 ≤ HSub.hSub (α := ℝ) (↑#ι : ℝ) 1
Tactic: classical
  /- For a function `f` in one variable and `t ∈ ℝ` we have
  `|f(t)| = `|∫_{-∞}^t Df(s)∂s| ≤ ∫_ℝ |Df(s)| ∂s` where we use the fundamental theorem of calculus.
  For each `x ∈ ℝⁿ` we let `u` vary in one of the `n` coordinates and apply the inequality above.
  By taking the product over these `n` factors, raising them to the power `(n-1)⁻¹` and integrating,
  we get the inequality `∫ |u| ^ (n/(n-1)) ≤ ∫ x, ∏ i, (∫ xᵢ, |Du(update x i xᵢ)|)^(n-1)⁻¹`.
  The result then follows from the grid-lines lemma. -/
  have : (1 : ℝ) ≤ ↑#ι - 1 := by
    have hι : (2 : ℝ) ≤ #ι := by exact_mod_cast hp.lt
    linarith
  calc ∫⁻ x, ‖u x‖ₑ ^ p
      = ∫⁻ x, (‖u x‖ₑ ^ (1 / (#ι - 1 : ℝ))) ^ (#ι : ℝ) := by
        -- a little algebraic manipulation of the exponent
        congr! 2 with x
        rw [← ENNReal.rpow_mul, hp.conjugate_eq]
        field_simp
    _ = ∫⁻ x, ∏ _i : ι, ‖u x‖ₑ ^ (1 / (#ι - 1 : ℝ)) := by
        -- express the left-hand integrand as a product of identical factors
        congr! 2 with x
        simp_rw [prod_const]
        norm_cast
    _ ≤ ∫⁻ x, ∏ i, (∫⁻ xᵢ, ‖fderiv ℝ u (update x i xᵢ)‖ₑ) ^ ((1 : ℝ) / (#ι - 1 : ℝ)) := ?_
    _ ≤ (∫⁻ x, ‖fderiv ℝ u x‖ₑ) ^ p := by
        -- apply the grid-lines lemma
        apply lintegral_prod_lintegral_pow_le _ hp
        fun_prop
  -- we estimate |u x| using the fundamental theorem of calculus.
  gcongr with x i
  calc ‖u x‖ₑ
    _ ≤ ∫⁻ xᵢ in Iic (x i), ‖deriv (u ∘ update x i) xᵢ‖ₑ := by
        apply le_trans (by simp) (HasCompactSupport.enorm_le_lintegral_Ici_deriv _ _ _)
        · exact hu.comp (by convert! contDiff_update 1 x i)
        · exact h2u.comp_isClosedEmbedding (isClosedEmbedding_update x i)
    _ ≤ ∫⁻ xᵢ, ‖fderiv ℝ u (update x i xᵢ)‖ₑ := ?_
  gcongr with y
  · exact Measure.restrict_le_self
  -- bound the derivative which appears
  calc ‖deriv (u ∘ update x i) y‖ₑ = ‖fderiv ℝ u (update x i y) (deriv (update x i) y)‖ₑ := by
        rw [fderiv_comp_deriv _ (hu.differentiable one_ne_zero).differentiableAt
          (hasDerivAt_update x i y).differentiableAt]
    _ ≤ ‖fderiv ℝ u (update x i y)‖ₑ * ‖deriv (update x i) y‖ₑ := ContinuousLinearMap.le_opENorm _ _
    _ ≤ ‖fderiv ℝ u (update x i y)‖ₑ := by simp [deriv_update, Pi.enorm_single]
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
ι : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Fintype ι
p : ℝ
hp : Real.HolderConjugate (↑#ι : ℝ) p
u : (ι → ℝ) → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
For : 1 ≤ HSub.hSub (α := ℝ) (↑#ι : ℝ) 1
⊢ ∫⁻ (x : ι → ℝ), ‖u x‖ₑ ^ p ≤
    (∫⁻ (x : ι → ℝ), enorm (E := ContinuousLinearMap.{0, 0, u_1, u_3} (RingHom.id ℝ) (ι → ℝ) F) (fderiv ℝ u x)) ^ p
have For₁ : ∀ (this : 1 ≤ HSub.hSub (α := ℝ) (↑#ι : ℝ) 1),
  ∫⁻ (x : ι → ℝ), ‖u x‖ₑ ^ p ≤
    (∫⁻ (x : ι → ℝ), enorm (E := ContinuousLinearMap.{0, 0, u_1, u_3} (RingHom.id ℝ) (ι → ℝ) F) (fderiv ℝ u x)) ^ p
Tactic: classical
  /- For a function `f` in one variable and `t ∈ ℝ` we have
  `|f(t)| = `|∫_{-∞}^t Df(s)∂s| ≤ ∫_ℝ |Df(s)| ∂s` where we use the fundamental theorem of calculus.
  For each `x ∈ ℝⁿ` we let `u` vary in one of the `n` coordinates and apply the inequality above.
  By taking the product over these `n` factors, raising them to the power `(n-1)⁻¹` and integrating,
  we get the inequality `∫ |u| ^ (n/(n-1)) ≤ ∫ x, ∏ i, (∫ xᵢ, |Du(update x i xᵢ)|)^(n-1)⁻¹`.
  The result then follows from the grid-lines lemma. -/
  have : (1 : ℝ) ≤ ↑#ι - 1 := by
    have hι : (2 : ℝ) ≤ #ι := by exact_mod_cast hp.lt
    linarith
  calc ∫⁻ x, ‖u x‖ₑ ^ p
      = ∫⁻ x, (‖u x‖ₑ ^ (1 / (#ι - 1 : ℝ))) ^ (#ι : ℝ) := by
        -- a little algebraic manipulation of the exponent
        congr! 2 with x
        rw [← ENNReal.rpow_mul, hp.conjugate_eq]
        field_simp
    _ = ∫⁻ x, ∏ _i : ι, ‖u x‖ₑ ^ (1 / (#ι - 1 : ℝ)) := by
        -- express the left-hand integrand as a product of identical factors
        congr! 2 with x
        simp_rw [prod_const]
        norm_cast
    _ ≤ ∫⁻ x, ∏ i, (∫⁻ xᵢ, ‖fderiv ℝ u (update x i xᵢ)‖ₑ) ^ ((1 : ℝ) / (#ι - 1 : ℝ)) := ?_
    _ ≤ (∫⁻ x, ‖fderiv ℝ u x‖ₑ) ^ p := by
        -- apply the grid-lines lemma
        apply lintegral_prod_lintegral_pow_le _ hp
        fun_prop
  -- we estimate |u x| using the fundamental theorem of calculus.
  gcongr with x i
  calc ‖u x‖ₑ
    _ ≤ ∫⁻ xᵢ in Iic (x i), ‖deriv (u ∘ update x i) xᵢ‖ₑ := by
        apply le_trans (by simp) (HasCompactSupport.enorm_le_lintegral_Ici_deriv _ _ _)
        · exact hu.comp (by convert! contDiff_update 1 x i)
        · exact h2u.comp_isClosedEmbedding (isClosedEmbedding_update x i)
    _ ≤ ∫⁻ xᵢ, ‖fderiv ℝ u (update x i xᵢ)‖ₑ := ?_
  gcongr with y
  · exact Measure.restrict_le_self
  -- bound the derivative which appears
  calc ‖deriv (u ∘ update x i) y‖ₑ = ‖fderiv ℝ u (update x i y) (deriv (update x i) y)‖ₑ := by
        rw [fderiv_comp_deriv _ (hu.differentiable one_ne_zero).differentiableAt
          (hasDerivAt_update x i y).differentiableAt]
    _ ≤ ‖fderiv ℝ u (update x i y)‖ₑ * ‖deriv (update x i) y‖ₑ := ContinuousLinearMap.le_opENorm _ _
    _ ≤ ‖fderiv ℝ u (update x i y)‖ₑ := by simp [deriv_update, Pi.enorm_single]
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
ι_1 : Type u_1
A : ι_1 → Type u_2
inst : (i : ι_1) → MeasurableSpace (A i)
μ_1 : (i : ι_1) → Measure (A i)
F : Type u_3
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
E : Type u_4
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
inst_7 : FiniteDimensional ℝ E
μ : Measure E
inst_8 : μ.IsAddHaarMeasure
p : ℝ
ι : Type := Fin (finrank ℝ E)
⊢ finrank ℝ E = finrank ℝ (ι → ℝ)
have rw : finrank ℝ E = #ι
Tactic: rw [finrank_fintype_fun_eq_card, Fintype.card_fin (finrank ℝ E)]
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
ι_1 : Type u_1
A : ι_1 → Type u_2
inst : (i : ι_1) → MeasurableSpace (A i)
μ_1 : (i : ι_1) → Measure (A i)
F : Type u_3
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
E : Type u_4
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
inst_7 : FiniteDimensional ℝ E
μ : Measure E
inst_8 : μ.IsAddHaarMeasure
p : ℝ
ι : Type := Fin (finrank ℝ E)
rw : finrank ℝ E = #ι
⊢ finrank ℝ E = finrank ℝ (ι → ℝ)
have rw₁ : finrank ℝ E = finrank ℝ E
Tactic: rw [finrank_fintype_fun_eq_card, Fintype.card_fin (finrank ℝ E)]
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (hypothesis)
Goal:
ι_1 : Type u_1
A : ι_1 → Type u_2
inst : (i : ι_1) → MeasurableSpace (A i)
μ_1 : (i : ι_1) → Measure (A i)
F : Type u_3
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
E : Type u_4
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
inst_7 : FiniteDimensional ℝ E
μ : Measure E
inst_8 : μ.IsAddHaarMeasure
p : ℝ
ι : Type := Fin (finrank ℝ E)
⊢ ℝ≥0
have this : finrank ℝ E = finrank ℝ (ι → ℝ)
Tactic: have : finrank ℝ E = finrank ℝ (ι → ℝ) := by
    rw [finrank_fintype_fun_eq_card, Fintype.card_fin (finrank ℝ E)]
-- 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 : Real.HolderConjugate (↑(finrank ℝ E) : ℝ) p
C : ℝ≥0 := lintegralPowLePowLIntegralFDerivConst μ p
ι : Type := Fin (finrank ℝ E)
⊢ ∫⁻ (x : E), ‖u x‖ₑ ^ p ∂μ ≤ (↑C : ℝ≥0∞) * (∫⁻ (x : E), enorm (E := E →L[ℝ] F) (fderiv ℝ u x) ∂μ) ^ p
have hιcard : #ι = finrank ℝ E
Tactic: have hιcard : #ι = finrank ℝ E := Fintype.card_fin (finrank ℝ E)
-- 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 : Real.HolderConjugate (↑(finrank ℝ E) : ℝ) p
C : ℝ≥0 := lintegralPowLePowLIntegralFDerivConst μ p
ι : Type := Fin (finrank ℝ E)
hιcard : #ι = finrank ℝ E
⊢ ∫⁻ (x : E), ‖u x‖ₑ ^ p ∂μ ≤ (↑C : ℝ≥0∞) * (∫⁻ (x : E), enorm (E := E →L[ℝ] F) (fderiv ℝ u x) ∂μ) ^ p
have this : finrank ℝ E = finrank ℝ (ι → ℝ)
Tactic: have : finrank ℝ E = finrank ℝ (ι → ℝ) := by simp [hιcard]
-- 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 : 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
⊢ ∫⁻ (x : E), ‖u x‖ₑ ^ p ∂μ ≤ (↑C : ℝ≥0∞) * (∫⁻ (x : E), enorm (E := E →L[ℝ] F) (fderiv ℝ u x) ∂μ) ^ p
have hp₁ : Real.HolderConjugate (↑#ι : ℝ) p
Tactic: have hp : Real.HolderConjugate #ι p := by rwa [hιcard]
-- 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
⊢ ∫⁻ (x : E), ‖u x‖ₑ ^ p ∂μ ≤ (↑C : ℝ≥0∞) * (∫⁻ (x : E), enorm (E := E →L[ℝ] F) (fderiv ℝ u x) ∂μ) ^ p
have h0p : 0 ≤ p
Tactic: have h0p : 0 ≤ p := hp.symm.nonneg
-- 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)
⊢ ∫⁻ (x : E), ‖u x‖ₑ ^ p ∂μ ≤ (↑C : ℝ≥0∞) * (∫⁻ (x : E), enorm (E := E →L[ℝ] F) (fderiv ℝ u x) ∂μ) ^ p
have hc : 0 < c
Tactic: have hc : 0 < c := addHaarScalarFactor_pos_of_isAddHaarMeasure ..
-- 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
⊢ ∫⁻ (x : E), ‖u x‖ₑ ^ p ∂μ ≤ (↑C : ℝ≥0∞) * (∫⁻ (x : E), enorm (E := E →L[ℝ] F) (fderiv ℝ u x) ∂μ) ^ p
have h2c : μ = HSMul.hSMul (β := Measure E) c (Measure.map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) volume)
Tactic: have h2c : μ = c • ((volume : Measure (ι → ℝ)).map e.symm) := isAddLeftInvariant_eq_smul ..
-- 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)
⊢ (↑c : ℝ≥0∞) ≠ 0
have simp_rw : ¬(↑c : ℝ≥0∞) = 0
Tactic: simp_rw [ne_eq, ENNReal.coe_eq_zero, hc.ne', not_false_eq_true]
-- 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
⊢ (↑c : ℝ≥0∞) ≠ 0
have simp_rw₁ : ¬c = 0
Tactic: simp_rw [ne_eq, ENNReal.coe_eq_zero, hc.ne', not_false_eq_true]