Documentation

MathlibNt.SieveTheory.LinearSieve.Suzuki.SuzukiCanonicalXiConstruction

source
noncomputable def Section10CanonicalXi.eta (x : ℝ) :
ℝ

The canonical function η(x)=∫₀¹ exp(tx)dt, including its removable value at zero.

Equations
Instances For
    Inspect dependencies

    Section10CanonicalXi.eta · compiled type and proof/definition references.

    source
    theorem Section10CanonicalXi.eta_eq_div {x : ℝ} (hx : x ≠ 0) :
    eta x = (Real.exp x - 1) / x
    Inspect dependencies

    Section10CanonicalXi.eta_eq_div · compiled type and proof/definition references.

    source
    @[simp]
    theorem Section10CanonicalXi.eta_zero :
    eta 0 = 1
    Inspect dependencies

    Section10CanonicalXi.eta_zero · compiled type and proof/definition references.

    source
    theorem Section10CanonicalXi.eta_continuous :
    Continuous eta
    Inspect dependencies

    Section10CanonicalXi.eta_continuous · compiled type and proof/definition references.

    source
    theorem Section10CanonicalXi.eta_hasDerivAt {x : ℝ} (hx : 0 < x) :
    HasDerivAt eta (eta x - (eta x - 1) / x) x
    Inspect dependencies

    Section10CanonicalXi.eta_hasDerivAt · compiled type and proof/definition references.

    source
    theorem Section10CanonicalXi.eta_slope_gt_half {x : ℝ} (hx : 0 < x) :
    1 / 2 < eta x - (eta x - 1) / x
    Inspect dependencies

    Section10CanonicalXi.eta_slope_gt_half · compiled type and proof/definition references.

    source
    theorem Section10CanonicalXi.eta_strictMonoOn :
    StrictMonoOn eta (Set.Ici 0)
    Inspect dependencies

    Section10CanonicalXi.eta_strictMonoOn · compiled type and proof/definition references.

    source
    theorem Section10CanonicalXi.eta_tendsto_atTop :
    Filter.Tendsto eta Filter.atTop Filter.atTop
    Inspect dependencies

    Section10CanonicalXi.eta_tendsto_atTop · compiled type and proof/definition references.

    source
    theorem Section10CanonicalXi.eta_image_Ici :
    eta '' Set.Ici 0 = Set.Ici 1
    Inspect dependencies

    Section10CanonicalXi.eta_image_Ici · compiled type and proof/definition references.

    source
    noncomputable def Section10CanonicalXi.etaOrderIso :
    ↑(Set.Ici 0) ≃o ↑(Set.Ici 1)

    Order isomorphism realizing the increasing inverse of η : [0,∞) → [1,∞).

    Equations
    Instances For
      Inspect dependencies

      Section10CanonicalXi.etaOrderIso · compiled type and proof/definition references.

      source
      theorem Section10CanonicalXi.etaOrderIso_apply (x : ↑(Set.Ici 0)) :
      ↑(etaOrderIso x) = eta ↑x
      Inspect dependencies

      Section10CanonicalXi.etaOrderIso_apply · compiled type and proof/definition references.

      source
      noncomputable def Section10CanonicalXi.xi (s : ℝ) :
      ℝ

      Canonical global extension: the positive inverse on (1,∞), and zero on (-∞,1].

      Equations
      Instances For
        Inspect dependencies

        Section10CanonicalXi.xi · compiled type and proof/definition references.

        source
        theorem Section10CanonicalXi.xi_continuous :
        Continuous xi
        Inspect dependencies

        Section10CanonicalXi.xi_continuous · compiled type and proof/definition references.

        source
        theorem Section10CanonicalXi.eta_xi (s : ℝ) :
        eta (xi s) = max s 1
        Inspect dependencies

        Section10CanonicalXi.eta_xi · compiled type and proof/definition references.

        source
        theorem Section10CanonicalXi.xi_pos {s : ℝ} (hs : 1 < s) :
        0 < xi s
        Inspect dependencies

        Section10CanonicalXi.xi_pos · compiled type and proof/definition references.

        source
        theorem Section10CanonicalXi.xi_equation {s : ℝ} (hs : 1 < s) :
        Real.exp (xi s) - 1 = s * xi s
        Inspect dependencies

        Section10CanonicalXi.xi_equation · compiled type and proof/definition references.

        source
        theorem Section10CanonicalXi.xi_differentiableAt {s : ℝ} (hs : 1 < s) :
        DifferentiableAt ℝ xi s
        Inspect dependencies

        Section10CanonicalXi.xi_differentiableAt · compiled type and proof/definition references.

        source
        theorem Section10CanonicalXi.xi_etaSlopeLower {s : ℝ} (hs : 1 < s) :
        1 / 2 < s - (s - 1) / xi s
        Inspect dependencies

        Section10CanonicalXi.xi_etaSlopeLower · compiled type and proof/definition references.

        source
        theorem Section10CanonicalXi.canonicalXi_proposition1020 :
        Section10Lemma1028.Proposition1020Xi xi

        The canonical inverse closes the exact weak Proposition 10.20 interface.

        Inspect dependencies

        Section10CanonicalXi.canonicalXi_proposition1020 · compiled type and proof/definition references.