Theorem: Super.potential_lt_one (Ray/Dynamics/Potential.lean)

State before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a✝ z : S
d n : ℕ
s : Super f d a✝
a : ∃ n, (c, (f c)^[n] z) ∈ s.near
⊢ s.potential c z < 1
Tactic:
simp only [Super.potential, a, dif_pos, Super.potential']
State after:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a✝ z : S
d n : ℕ
s : Super f d a✝
a : ∃ n, (c, (f c)^[n] z) ∈ s.near
⊢ Complex.abs (s.bottcherNear c ((f c)^[Nat.find ⋯] z)) ^ (↑d ^ Nat.find ⋯)⁻¹ < 1

State before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a✝ z : S
d n : ℕ
s : Super f d a✝
a : ∃ n, (c, (f c)^[n] z) ∈ s.near
⊢ Complex.abs (s.bottcherNear c ((f c)^[Nat.find ⋯] z)) ^ (↑d ^ Nat.find ⋯)⁻¹ < 1
Tactic:
refine Real.rpow_lt_one (Complex.abs.nonneg _) ?_ (by bound)
State after:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a✝ z : S
d n : ℕ
s : Super f d a✝
a : ∃ n, (c, (f c)^[n] z) ∈ s.near
⊢ Complex.abs (s.bottcherNear c ((f c)^[Nat.find ⋯] z)) < 1

State before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a✝ z : S
d n : ℕ
s : Super f d a✝
a : ∃ n, (c, (f c)^[n] z) ∈ s.near
⊢ Complex.abs (s.bottcherNear c ((f c)^[Nat.find ⋯] z)) < 1
Tactic:
exact s.bottcherNear_lt_one (Nat.find_spec a)
State after:
no goals

State before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a✝ z : S
d n : ℕ
s : Super f d a✝
a : ∃ n, (c, (f c)^[n] z) ∈ s.near
⊢ 0 < (↑d ^ Nat.find ⋯)⁻¹
Tactic:
bound
State after:
no goals