HomogeneousTransgressionFTC.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Mahler.MassHypotheses.homogeneousResidualFlux_eq_zero_of_transgression line 14

theorem OAI.Mahler.MassHypotheses.homogeneousPathFlux_constant_of_transgression line 34

Source documentation

The fundamental theorem of calculus with an explicit local transgression formula. The local algebraic identity is retained as a conditional premise.

theorem MassHypotheses.homogeneousPathFlux_constant_of_transgression {k N m : ℕ}
    {U : Set (ComplexEuclidean (k+2))} {f : Fin N → ComplexEuclidean (k+2) → ℂ}
    {G : Fin N → MvPolynomial (Fin (k+2)) ℂ} (h : MassHypotheses (k+2) N m U f G)
    (ht : ∀ (t : ℝ) (x : ComplexEuclidean (k+2)), ‖x‖ = 1 →
      ∀ v : Fin (2*(k+1)+1) → ComplexEuclidean (k+2),
      (∀ i, inner ℝ x (v i) = 0) →
      boundaryResidualFin (alphaPath (polynomialMap G) (coordinateMap (k+2)) m t)
        (betaLinear (polynomialMap G) (coordinateMap (k+2)) m) x v =
        -((k+1 : ℕ) : ℂ) * extDeriv (sourceHomogeneousPrimitive (m := m) G t) x v)
…

Mentions: OAI.Mahler.ComplexEuclidean, OAI.Mahler.MassHypotheses, OAI.Mahler.boundaryResidualFin, OAI.Mahler.alphaPath, OAI.Mahler.polynomialMap, OAI.Mahler.coordinateMap, OAI.Mahler.betaLinear, OAI.Mahler.sourceHomogeneousPrimitive

theorem OAI.Mahler.MassHypotheses.homogeneousFlux_endpoints_of_transgression line 51

Source documentation

Both flux endpoints follow from the explicit local formula. This theorem retains the local transgression identity as a hypothesis.

theorem MassHypotheses.homogeneousFlux_endpoints_of_transgression {k N m : ℕ}
    {U : Set (ComplexEuclidean (k+2))} {f : Fin N → ComplexEuclidean (k+2) → ℂ}
    {G : Fin N → MvPolynomial (Fin (k+2)) ℂ} (h : MassHypotheses (k+2) N m U f G)
    (ht : ∀ (t : ℝ) (x : ComplexEuclidean (k+2)), ‖x‖ = 1 →
      ∀ v : Fin (2*(k+1)+1) → ComplexEuclidean (k+2),
      (∀ i, inner ℝ x (v i) = 0) →
      boundaryResidualFin (alphaPath (polynomialMap G) (coordinateMap (k+2)) m t)
        (betaLinear (polynomialMap G) (coordinateMap (k+2)) m) x v =
        -((k+1 : ℕ) : ℂ) * extDeriv (sourceHomogeneousPrimitive (m := m) G t) x v) :
…

theorem OAI.Mahler.MassHypotheses.small_sphere_real_flux_limit_one line 68