Theorems · Theorem · real analysis

logDeriv_eqOn_iff

∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] [IsRCLikeNormedField 𝕜] {f g : 𝕜 → 𝕜'} {s : Set 𝕜},
  DifferentiableOn 𝕜 f s →
    DifferentiableOn 𝕜 g s →
      IsOpen s →
        IsPreconnected s →
          (∀ x ∈ s, g x ≠ 0) →
            (∀ x ∈ s, f x ≠ 0) → (Set.EqOn (logDeriv f) (logDeriv g) s ↔ ∃ z, z ≠ 0 ∧ Set.EqOn f (z • g) s)

Defined in

Mathlib.Analysis.Calculus.LogDeriv

Cited by

0 results in Mathlib

Foundations

Depth 197 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NontriviallyNormedFieldNontriviallyNormedFieldNormedAlgebraIsRCLikeNormedField