awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : IsStrictlyPositive a
p : ℝ
funProp : 0 ≤ p
funProp₁ : (↑0 : ℝ) ≤ p
⊢ ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) (spectrum ℝ a)
have funProp₂ : ∀ x ∈ spectrum ℝ a, x ≠ 0
Tactic: fun_prop (disch := grind -abstractProof)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order (hypothesis)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : IsStrictlyPositive a
s : Set A := {a : A | IsStrictlyPositive a}
f : (p x : ℝ) → ℝ := fun (p x : ℝ) ↦ if p > 0 then p⁻¹ * (x ^ p - 1) else Real.log x
⊢ TendstoUniformlyOn (fun (p x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) Real.log (𝓝[>] 0) (spectrum ℝ a)
have hmain : TendstoLocallyUniformlyOn (fun (p x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) Real.log (𝓝[>] 0) (Set.Ioi 0)
Tactic: have hmain := Real.tendstoLocallyUniformlyOn_rpow_sub_one_log
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order (hypothesis)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : IsStrictlyPositive a
s : Set A := {a : A | IsStrictlyPositive a}
f : (p x : ℝ) → ℝ := fun (p x : ℝ) ↦ if p > 0 then p⁻¹ * (x ^ p - 1) else Real.log x
hmain : TendstoLocallyUniformlyOn (fun (p x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) Real.log (𝓝[>] 0) (Set.Ioi 0)
⊢ TendstoUniformlyOn (fun (p x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) Real.log (𝓝[>] 0) (spectrum ℝ a)
have hmain₁ : ∀ K ⊆ Set.Ioi 0, IsCompact K → TendstoUniformlyOn (fun (p x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) Real.log (𝓝[>] 0) K
Tactic: rw [tendstoLocallyUniformlyOn_iff_forall_isCompact isOpen_Ioi] at hmain
Cleared hypotheses: hmain
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : IsStrictlyPositive a
case case₁ case₂ case₃ : TendstoUniformlyOn (fun (p x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) Real.log (𝓝[>] 0) (spectrum ℝ a)
⊢ TendstoUniformlyOn (fun (p x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) Real.log (𝓝[>] 0) (spectrum ℝ a)
have case₄ : ∀ (hmain : TendstoLocallyUniformlyOn (fun (p x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) Real.log (𝓝[>] 0) (Set.Ioi 0)),
  TendstoUniformlyOn (fun (p x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) Real.log (𝓝[>] 0) (spectrum ℝ a)
Tactic: case tendsto =>
    let s := {a : A | IsStrictlyPositive a}
    let f (p : ℝ) (x : ℝ) := if p > 0 then p⁻¹ * (x ^ p - 1) else Real.log x
    have hmain := Real.tendstoLocallyUniformlyOn_rpow_sub_one_log
    rw [tendstoLocallyUniformlyOn_iff_forall_isCompact isOpen_Ioi] at hmain
    exact hmain (spectrum ℝ a) (by grind) (by grind)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : IsStrictlyPositive a
case case₁ case₂ case₃ : TendstoUniformlyOn (fun (p x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) Real.log (𝓝[>] 0) (spectrum ℝ a)
case₄ :
  ∀ (hmain : TendstoLocallyUniformlyOn (fun (p x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) Real.log (𝓝[>] 0) (Set.Ioi 0)),
    TendstoUniformlyOn (fun (p x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) Real.log (𝓝[>] 0) (spectrum ℝ a)
⊢ TendstoUniformlyOn (fun (p x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) Real.log (𝓝[>] 0) (spectrum ℝ a)
have case₅ : ∀ (hmain : ∀ K ⊆ Set.Ioi 0, IsCompact K → TendstoUniformlyOn (fun (p x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) Real.log (𝓝[>] 0) K),
  TendstoUniformlyOn (fun (p x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) Real.log (𝓝[>] 0) (spectrum ℝ a)
Tactic: case tendsto =>
    let s := {a : A | IsStrictlyPositive a}
    let f (p : ℝ) (x : ℝ) := if p > 0 then p⁻¹ * (x ^ p - 1) else Real.log x
    have hmain := Real.tendstoLocallyUniformlyOn_rpow_sub_one_log
    rw [tendstoLocallyUniformlyOn_iff_forall_isCompact isOpen_Ioi] at hmain
    exact hmain (spectrum ℝ a) (by grind) (by grind)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
⊢ Tendsto.{0, u_1} (β := (a : A) → A)
    (fun (p : ℝ) (a : A) ↦
      if Membership.mem (γ := Set A) {b : A | IsStrictlyPositive b} a then
        cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) a
      else 0)
    (𝓝[>] 0) (𝓝 fun (a : A) ↦ if Membership.mem (γ := Set A) {b : A | IsStrictlyPositive b} a then log a else 0)
have rw : ∀ (x : A),
  Tendsto
    (fun (i : ℝ) ↦
      if Membership.mem (γ := Set A) {b : A | IsStrictlyPositive b} x then
        cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ i⁻¹ * (x ^ i - 1)) x
      else 0)
    (𝓝[>] 0) (𝓝 (if Membership.mem (γ := Set A) {b : A | IsStrictlyPositive b} x then log x else 0))
Tactic: rw [tendsto_pi_nhds]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
⊢ Tendsto
    (fun (i : ℝ) ↦
      if Membership.mem (γ := Set A) {b : A | IsStrictlyPositive b} a then
        cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ i⁻¹ * (x ^ i - 1)) a
      else 0)
    (𝓝[>] 0) (𝓝 (if Membership.mem (γ := Set A) {b : A | IsStrictlyPositive b} a then log a else 0))
have pos : ∀ (ha : IsStrictlyPositive a),
  Tendsto
    (fun (i : ℝ) ↦
      if Membership.mem (γ := Set A) {b : A | IsStrictlyPositive b} a then
        cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ i⁻¹ * (x ^ i - 1)) a
      else 0)
    (𝓝[>] 0) (𝓝 (if Membership.mem (γ := Set A) {b : A | IsStrictlyPositive b} a then log a else 0))
Tactic: by_cases ha : IsStrictlyPositive a
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
pos :
  ∀ (ha : IsStrictlyPositive a),
    Tendsto
      (fun (i : ℝ) ↦
        if Membership.mem (γ := Set A) {b : A | IsStrictlyPositive b} a then
          cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ i⁻¹ * (x ^ i - 1)) a
        else 0)
      (𝓝[>] 0) (𝓝 (if Membership.mem (γ := Set A) {b : A | IsStrictlyPositive b} a then log a else 0))
⊢ Tendsto
    (fun (i : ℝ) ↦
      if Membership.mem (γ := Set A) {b : A | IsStrictlyPositive b} a then
        cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ i⁻¹ * (x ^ i - 1)) a
      else 0)
    (𝓝[>] 0) (𝓝 (if Membership.mem (γ := Set A) {b : A | IsStrictlyPositive b} a then log a else 0))
have neg : ∀ (ha : ¬IsStrictlyPositive a),
  Tendsto
    (fun (i : ℝ) ↦
      if Membership.mem (γ := Set A) {b : A | IsStrictlyPositive b} a then
        cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ i⁻¹ * (x ^ i - 1)) a
      else 0)
    (𝓝[>] 0) (𝓝 (if Membership.mem (γ := Set A) {b : A | IsStrictlyPositive b} a then log a else 0))
Tactic: by_cases ha : IsStrictlyPositive a
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ
a : A
ha : Membership.mem (γ := Set A) {a : A | IsStrictlyPositive a} a
⊢ Eq.{u_1 + 1} (α := A)
    ((fun (a : A) ↦
        if Membership.mem (γ := Set A) {b : A | IsStrictlyPositive b} a then
          cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) a
        else 0)
      a)
    ((fun (a : A) ↦ p⁻¹ • (a ^ p - 1)) a)
have simp : cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ p⁻¹ • (x ^ p - 1)) a = p⁻¹ • (a ^ p - 1)
Tactic: simp only [ha, ↓reduceIte, ← smul_eq_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ
a : A
ha : Membership.mem (γ := Set A) {a : A | IsStrictlyPositive a} a
⊢ ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ x ^ p - 1) (spectrum ℝ a)
have funProp : 0 ≤ p
Tactic: fun_prop (disch := grind)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ
a : A
ha : Membership.mem (γ := Set A) {a : A | IsStrictlyPositive a} a
funProp : 0 ≤ p
⊢ ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ x ^ p - 1) (spectrum ℝ a)
have funProp₁ : (↑0 : ℝ) ≤ p
Tactic: fun_prop (disch := grind)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ
a : A
ha : Membership.mem (γ := Set A) {a : A | IsStrictlyPositive a} a
funProp : 0 ≤ p
funProp₁ : (↑0 : ℝ) ≤ p
⊢ ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ x ^ p - 1) (spectrum ℝ a)
have funProp₂ : ∀ x ∈ spectrum ℝ a, x ≠ 0
Tactic: fun_prop (disch := grind)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ
a : A
ha : Membership.mem (γ := Set A) {a : A | IsStrictlyPositive a} a
⊢ ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ x ^ p) (spectrum ℝ a)
have funProp : 0 ≤ p
Tactic: fun_prop (disch := grind)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ
a : A
ha : Membership.mem (γ := Set A) {a : A | IsStrictlyPositive a} a
funProp : 0 ≤ p
⊢ ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ x ^ p) (spectrum ℝ a)
have funProp₁ : (↑0 : ℝ) ≤ p
Tactic: fun_prop (disch := grind)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ
a : A
ha : Membership.mem (γ := Set A) {a : A | IsStrictlyPositive a} a
funProp : 0 ≤ p
funProp₁ : (↑0 : ℝ) ≤ p
⊢ ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ x ^ p) (spectrum ℝ a)
have funProp₂ : ∀ x ∈ spectrum ℝ a, x ≠ 0
Tactic: fun_prop (disch := grind)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ
a : A
ha : Membership.mem (γ := Set A) {a : A | IsStrictlyPositive a} a
⊢ cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ p⁻¹ • (x ^ p - 1)) a = p⁻¹ • (a ^ p - 1)
have rw : p⁻¹ • cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x ^ p - 1) a = p⁻¹ • (a ^ p - 1)
Tactic: rw [cfc_smul _ (hf := by fun_prop (disch := grind)),
    cfc_sub _ _ (hf := by fun_prop (disch := grind)),
    cfc_const_one .., rpow_eq_cfc_real ..]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ
a : A
ha : Membership.mem (γ := Set A) {a : A | IsStrictlyPositive a} a
rw : p⁻¹ • cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x ^ p - 1) a = p⁻¹ • (a ^ p - 1)
⊢ cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ p⁻¹ • (x ^ p - 1)) a = p⁻¹ • (a ^ p - 1)
have rw₁ : p⁻¹ • (cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x ^ p) a - cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ 1) a) =
  p⁻¹ • (a ^ p - 1)
Tactic: rw [cfc_smul _ (hf := by fun_prop (disch := grind)),
    cfc_sub _ _ (hf := by fun_prop (disch := grind)),
    cfc_const_one .., rpow_eq_cfc_real ..]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ
a : A
ha : Membership.mem (γ := Set A) {a : A | IsStrictlyPositive a} a
rw : p⁻¹ • cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x ^ p - 1) a = p⁻¹ • (a ^ p - 1)
rw₁ :
  p⁻¹ • (cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x ^ p) a - cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ 1) a) =
    p⁻¹ • (a ^ p - 1)
⊢ cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ p⁻¹ • (x ^ p - 1)) a = p⁻¹ • (a ^ p - 1)
have rw₂ : p⁻¹ • (cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x ^ p) a - 1) = p⁻¹ • (a ^ p - 1)
Tactic: rw [cfc_smul _ (hf := by fun_prop (disch := grind)),
    cfc_sub _ _ (hf := by fun_prop (disch := grind)),
    cfc_const_one .., rpow_eq_cfc_real ..]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ
a : A
ha : Membership.mem (γ := Set A) {a : A | IsStrictlyPositive a} a
rw : p⁻¹ • cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x ^ p - 1) a = p⁻¹ • (a ^ p - 1)
rw₁ :
  p⁻¹ • (cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x ^ p) a - cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ 1) a) =
    p⁻¹ • (a ^ p - 1)
rw₂ : p⁻¹ • (cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x ^ p) a - 1) = p⁻¹ • (a ^ p - 1)
⊢ cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ p⁻¹ • (x ^ p - 1)) a = p⁻¹ • (a ^ p - 1)
have rw₃ : p⁻¹ • (cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x ^ p) a - 1) =
  p⁻¹ • (cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x ^ p) a - 1)
Tactic: rw [cfc_smul _ (hf := by fun_prop (disch := grind)),
    cfc_sub _ _ (hf := by fun_prop (disch := grind)),
    cfc_const_one .., rpow_eq_cfc_real ..]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order (hypothesis)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
s : Set A := {a : A | IsStrictlyPositive a}
f : (p : ℝ) → (a : A) → A :=
  fun (p : ℝ) (a : A) ↦ if a ∈ s then cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) a else 0
g : (a : A) → A := fun (a : A) ↦ if a ∈ s then log a else 0
⊢ MonotoneOn log {a : A | IsStrictlyPositive a}
have hg : Set.EqOn g log s
Tactic: have hg : s.EqOn g (log (A := A)) := by simp +contextual [g, Set.EqOn]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
s : Set A := {a : A | IsStrictlyPositive a}
f : (p : ℝ) → (a : A) → A :=
  fun (p : ℝ) (a : A) ↦ if a ∈ s then cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) a else 0
g : (a : A) → A := fun (a : A) ↦ if a ∈ s then log a else 0
hg : Set.EqOn g log s
⊢ MonotoneOn log {a : A | IsStrictlyPositive a}
have refine : MonotoneOn g {a : A | IsStrictlyPositive a}
Tactic: refine MonotoneOn.congr ?_ hg
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
s : Set A := {a : A | IsStrictlyPositive a}
f : (p : ℝ) → (a : A) → A :=
  fun (p : ℝ) (a : A) ↦ if a ∈ s then cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) a else 0
g : (a : A) → A := fun (a : A) ↦ if a ∈ s then log a else 0
hg : Set.EqOn g log s
⊢ MonotoneOn g {a : A | IsStrictlyPositive a}
have refine : ∀ᶠ (x : ℝ) in 𝓝[>] 0,
  Membership.mem (γ := Set ((a : A) → A)) {f : A → A | MonotoneOn f {a : A | IsStrictlyPositive a}} (f x)
Tactic: refine isClosed_monotoneOn.mem_of_tendsto (f := f) (b := (𝓝[>] 0))
    tendsto_ite_cfc_rpow_sub_one_ite_log ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order (hypothesis)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
s : Set A := {a : A | IsStrictlyPositive a}
f : (p : ℝ) → (a : A) → A :=
  fun (p : ℝ) (a : A) ↦ if a ∈ s then cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) a else 0
g : (a : A) → A := fun (a : A) ↦ if a ∈ s then log a else 0
hg : Set.EqOn g log s
⊢ ∀ᶠ (x : ℝ) in 𝓝[>] 0,
    Membership.mem (γ := Set ((a : A) → A)) {f : A → A | MonotoneOn f {a : A | IsStrictlyPositive a}} (f x)
have h₁ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, 0 < p ∧ p < 1
Tactic: have h₁ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, 0 < p ∧ p < 1 := nhdsGT_basis 0 |>.mem_of_mem zero_lt_one
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
s : Set A := {a : A | IsStrictlyPositive a}
f : (p : ℝ) → (a : A) → A :=
  fun (p : ℝ) (a : A) ↦ if a ∈ s then cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) a else 0
g : (a : A) → A := fun (a : A) ↦ if a ∈ s then log a else 0
hg : Set.EqOn g log s
h₁ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, 0 < p ∧ p < 1
p : ℝ
⊢ 0 < p ∧ p < 1 → MonotoneOn (f p) {a : A | IsStrictlyPositive a}
have h : ∀ (hp : 0 < p) (hp' : p < 1), MonotoneOn (f p) {a : A | IsStrictlyPositive a}
Tactic: ⟨hp, hp'⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
s : Set A := {a : A | IsStrictlyPositive a}
f : (p : ℝ) → (a : A) → A :=
  fun (p : ℝ) (a : A) ↦ if a ∈ s then cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) a else 0
g : (a : A) → A := fun (a : A) ↦ if a ∈ s then log a else 0
hg : Set.EqOn g log s
h₁ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, 0 < p ∧ p < 1
⊢ ∀ᶠ (x : ℝ) in 𝓝[>] 0,
    Membership.mem (γ := Set ((a : A) → A)) {f : A → A | MonotoneOn f {a : A | IsStrictlyPositive a}} (f x)
have h : ∀ (p : ℝ) (hp : 0 < p) (hp' : p < 1), MonotoneOn (f p) {a : A | IsStrictlyPositive a}
Tactic: filter_upwards [h₁] with p ⟨hp, hp'⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
s : Set A := {a : A | IsStrictlyPositive a}
f : (p : ℝ) → (a : A) → A :=
  fun (p : ℝ) (a : A) ↦ if a ∈ s then cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) a else 0
g : (a : A) → A := fun (a : A) ↦ if a ∈ s then log a else 0
hg : Set.EqOn g log s
h₁ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, 0 < p ∧ p < 1
p : ℝ
hp : 0 < p
hp' : p < 1
⊢ MonotoneOn (f p) {a : A | IsStrictlyPositive a}
have h : ∀ (a : A) (ha : Membership.mem (γ := Set A) {a : A | IsStrictlyPositive a} a) (b : A)
  (hb : Membership.mem (γ := Set A) {a : A | IsStrictlyPositive a} b) (hab : a ≤ b),
  p⁻¹ • (a ^ p - 1) ≤ p⁻¹ • (b ^ p - 1)
Tactic: refine MonotoneOn.congr (fun a ha b hb hab ↦ ?_) CFC.cfc_rpow_sub_one_eqOn.symm
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
s : Set A := {a : A | IsStrictlyPositive a}
f : (p : ℝ) → (a : A) → A :=
  fun (p : ℝ) (a : A) ↦ if a ∈ s then cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) a else 0
g : (a : A) → A := fun (a : A) ↦ if a ∈ s then log a else 0
hg : Set.EqOn g log s
h₁ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, 0 < p ∧ p < 1
p : ℝ
hp : 0 < p
hp' : p < 1
a : A
ha : Membership.mem (γ := Set A) {a : A | IsStrictlyPositive a} a
b : A
hb : Membership.mem (γ := Set A) {a : A | IsStrictlyPositive a} b
hab : a ≤ b
⊢ p⁻¹ • (a ^ p - 1) ≤ p⁻¹ • (b ^ p - 1)
have h : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) p
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order (hypothesis)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
s : Set A := {a : A | IsStrictlyPositive a}
f : (p : ℝ) → (a : A) → A :=
  fun (p : ℝ) (a : A) ↦ if a ∈ s then cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) a else 0
g : (a : A) → A := fun (a : A) ↦ if a ∈ s then log a else 0
⊢ ConcaveOn ℝ s log
have hg : EqOn g log s
Tactic: have hg : s.EqOn g (log (A := A)) := by simp +contextual [g, Set.EqOn]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
s : Set A := {a : A | IsStrictlyPositive a}
f : (p : ℝ) → (a : A) → A :=
  fun (p : ℝ) (a : A) ↦ if a ∈ s then cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) a else 0
g : (a : A) → A := fun (a : A) ↦ if a ∈ s then log a else 0
hg : EqOn g log s
⊢ ConcaveOn ℝ s log
have refine : ConcaveOn ℝ s g
Tactic: refine ConcaveOn.congr ?_ hg
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
s : Set A := {a : A | IsStrictlyPositive a}
f : (p : ℝ) → (a : A) → A :=
  fun (p : ℝ) (a : A) ↦ if a ∈ s then cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) a else 0
g : (a : A) → A := fun (a : A) ↦ if a ∈ s then log a else 0
hg : EqOn g log s
⊢ ConcaveOn ℝ s g
have apply : ∀ᶠ (x : ℝ) in 𝓝[>] 0, Membership.mem (γ := Set ((a : A) → A)) {f : A → A | ConcaveOn ℝ s f} (f x)
Tactic: apply isClosed_setOf_concaveOn.mem_of_tendsto (f := f) (b := (𝓝[>] (0 : ℝ)))
    tendsto_ite_cfc_rpow_sub_one_ite_log ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order (hypothesis)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
s : Set A := {a : A | IsStrictlyPositive a}
f : (p : ℝ) → (a : A) → A :=
  fun (p : ℝ) (a : A) ↦ if a ∈ s then cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) a else 0
g : (a : A) → A := fun (a : A) ↦ if a ∈ s then log a else 0
hg : EqOn g log s
⊢ ∀ᶠ (x : ℝ) in 𝓝[>] 0, Membership.mem (γ := Set ((a : A) → A)) {f : A → A | ConcaveOn ℝ s f} (f x)
have h₁ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, 0 < p ∧ p < 1
Tactic: have h₁ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, 0 < p ∧ p < 1 := nhdsGT_basis 0 |>.mem_of_mem zero_lt_one
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
s : Set A := {a : A | IsStrictlyPositive a}
f : (p : ℝ) → (a : A) → A :=
  fun (p : ℝ) (a : A) ↦ if a ∈ s then cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) a else 0
g : (a : A) → A := fun (a : A) ↦ if a ∈ s then log a else 0
hg : EqOn g log s
h₁ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, 0 < p ∧ p < 1
p : ℝ
⊢ 0 < p ∧ p < 1 → ConcaveOn ℝ s (f p)
have h : ∀ (hp : 0 < p) (hp' : p < 1), ConcaveOn ℝ s (f p)
Tactic: ⟨hp, hp'⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
s : Set A := {a : A | IsStrictlyPositive a}
f : (p : ℝ) → (a : A) → A :=
  fun (p : ℝ) (a : A) ↦ if a ∈ s then cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) a else 0
g : (a : A) → A := fun (a : A) ↦ if a ∈ s then log a else 0
hg : EqOn g log s
h₁ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, 0 < p ∧ p < 1
⊢ ∀ᶠ (x : ℝ) in 𝓝[>] 0, Membership.mem (γ := Set ((a : A) → A)) {f : A → A | ConcaveOn ℝ s f} (f x)
have h : ∀ (p : ℝ) (hp : 0 < p) (hp' : p < 1), ConcaveOn ℝ s (f p)
Tactic: filter_upwards [h₁] with p ⟨hp, hp'⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
s : Set A := {a : A | IsStrictlyPositive a}
f : (p : ℝ) → (a : A) → A :=
  fun (p : ℝ) (a : A) ↦ if a ∈ s then cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ p⁻¹ * (x ^ p - 1)) a else 0
g : (a : A) → A := fun (a : A) ↦ if a ∈ s then log a else 0
hg : EqOn g log s
h₁ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, 0 < p ∧ p < 1
p : ℝ
hp : 0 < p
hp' : p < 1
⊢ ConcaveOn ℝ s (f p)
have h : ConcaveOn ℝ (β := A) s fun (a : A) ↦ p⁻¹ • (a ^ p - 1)
Tactic: refine ConcaveOn.congr ?_ CFC.cfc_rpow_sub_one_eqOn.symm