Documentation

LeanPool.PlanarMidpoint.ExceptionalGeometry

The two exceptional cubic graphs #

The rational graphs are defined everywhere, but all calculus statements carry an explicit nonzero trace hypothesis. Their tangent maps are given in fixed Euclidean coordinates.

source
def PlanarMidpoint.radiusSq (τ : E) :
ℝ

The squared Euclidean length of the trace vector.

Equations
Instances For
    source
    noncomputable def PlanarMidpoint.Q (τ : E) :
    Coeff

    The pure-cube exceptional graph, extended by zero at zero trace.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def PlanarMidpoint.R (τ : E) :
      Coeff

      The second exceptional cubic graph, extended by zero at zero trace.

      Equations
      Instances For
        source
        theorem PlanarMidpoint.radiusSq_pos {τ : E} (hτ : τ ≠ 0) :
        0 < radiusSq τ
        source
        theorem PlanarMidpoint.radiusSq_ne_zero {τ : E} (hτ : τ ≠ 0) :
        radiusSq τ ≠ 0
        source
        theorem PlanarMidpoint.trace_Q {τ : E} (hτ : τ ≠ 0) :
        trace (Q τ) = τ
        source
        theorem PlanarMidpoint.trace_R {τ : E} (hτ : τ ≠ 0) :
        trace (R τ) = τ
        source
        theorem PlanarMidpoint.cubic_Q_trace {τ : E} (hτ : τ ≠ 0) :
        cubic (Q τ) τ τ τ = radiusSq τ ^ 2
        source
        theorem PlanarMidpoint.cubic_R_trace {τ : E} (hτ : τ ≠ 0) :
        cubic (R τ) τ τ τ = 0
        source
        theorem PlanarMidpoint.Q_ne_R {τ : E} (hτ : τ ≠ 0) :
        Q τ ≠ R τ
        source
        noncomputable def PlanarMidpoint.pr (i : Fin 2) :
        E →L[ℝ] ℝ

        Continuous linear evaluation of a standard Euclidean coordinate.

        Equations
        Instances For
          source
          def PlanarMidpoint.QNum (τ : E) :
          Fin 4 → Fin 2 → ℝ

          Numerators of the four rows of the derivative of Q.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            noncomputable def PlanarMidpoint.QDeriv (τ : E) :
            E →L[ℝ] Coeff

            The derivative of the pure-cube graph away from zero trace.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              theorem PlanarMidpoint.QDeriv_apply (τ v : E) (i : Fin 4) :
              (QDeriv τ) v i = (QNum τ i 0 * v.ofLp 0 + QNum τ i 1 * v.ofLp 1) / radiusSq τ ^ 2
              source
              theorem PlanarMidpoint.hasFDerivAt_Q {τ : E} (hτ : τ ≠ 0) :
              HasFDerivAt Q (QDeriv τ) τ
              source
              noncomputable def PlanarMidpoint.linearR :
              E →L[ℝ] Coeff

              The linear part of the second exceptional graph.

              Equations
              Instances For
                source
                noncomputable def PlanarMidpoint.RDeriv (τ : E) :
                E →L[ℝ] Coeff

                The derivative of the second exceptional graph away from zero trace.

                Equations
                Instances For
                  source
                  def PlanarMidpoint.RNum (τ : E) :
                  Fin 4 → Fin 2 → ℝ

                  Numerators of the tangent map to the second exceptional graph.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    theorem PlanarMidpoint.hasFDerivAt_R {τ : E} (hτ : τ ≠ 0) :
                    HasFDerivAt R (RDeriv τ) τ
                    source
                    theorem PlanarMidpoint.RDeriv_apply {τ : E} (hτ : τ ≠ 0) (v : E) (i : Fin 4) :
                    (RDeriv τ) v i = (RNum τ i 0 * v.ofLp 0 + RNum τ i 1 * v.ofLp 1) / radiusSq τ ^ 2
                    source
                    def PlanarMidpoint.traceCLM :
                    Coeff →L[ℝ] E

                    The trace map is a fixed continuous linear map.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      @[simp]
                      theorem PlanarMidpoint.traceCLM_apply (c : Coeff) :
                      traceCLM c = trace c
                      source
                      theorem PlanarMidpoint.continuous_trace :
                      Continuous trace
                      source
                      theorem PlanarMidpoint.differentiableAt_Q {τ : E} (hτ : τ ≠ 0) :
                      DifferentiableAt ℝ Q τ
                      source
                      theorem PlanarMidpoint.differentiableAt_R {τ : E} (hτ : τ ≠ 0) :
                      DifferentiableAt ℝ R τ
                      source
                      theorem PlanarMidpoint.continuousAt_Q {τ : E} (hτ : τ ≠ 0) :
                      ContinuousAt Q τ
                      source
                      theorem PlanarMidpoint.continuousAt_R {τ : E} (hτ : τ ≠ 0) :
                      ContinuousAt R τ
                      source
                      theorem PlanarMidpoint.norm_Q_le (τ : E) :
                      ‖Q τ‖ ≤ ‖τ‖
                      source
                      @[simp]
                      theorem PlanarMidpoint.Q_zero :
                      Q 0 = 0
                      source
                      @[simp]
                      theorem PlanarMidpoint.R_zero :
                      R 0 = 0
                      source
                      theorem PlanarMidpoint.continuous_Q :
                      Continuous Q

                      The rational expression has a continuous extension through the zero trace.

                      source
                      theorem PlanarMidpoint.continuous_R :
                      Continuous R