OAI/Analysis/Mahler/HomogeneousFluxDifferentiation.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Mahler.contDiffAt_dcLinear_one line 12
2. lemma OAI.Mahler.continuous_sphere_oneForm line 19
3. lemma OAI.Mahler.continuous_sphere_extDeriv line 27
4. lemma OAI.Mahler.continuous_sphere_affine_oneForm_eval line 41
5. lemma OAI.Mahler.continuous_sphere_affine_extDeriv_eval line 53
6. lemma OAI.Mahler.continuous_wedgePowerVariation_eval line 71
7. lemma OAI.Mahler.continuous_sphere_affine_boundary_eval line 84
8. lemma OAI.Mahler.continuous_sphere_affine_residual_eval line 97
9. lemma OAI.Mahler.MassHypotheses.homogeneous_path_C1 line 114
10. theorem OAI.Mahler.MassHypotheses.homogeneousPathFlux_hasDerivAt line 145

    Source documentation

    The homogeneous flux has the residual flux as derivative, from the mass hypotheses. No integral regularity premise remains. The residual integral is retained; this theorem does not assert it is zero.

    theorem MassHypotheses.homogeneousPathFlux_hasDerivAt {k N m : ℕ}
        {U : Set (ComplexEuclidean (k+1))} {f : Fin N → ComplexEuclidean (k+1) → ℂ}
        {G : Fin N → MvPolynomial (Fin (k+1)) ℂ} (h : MassHypotheses (k+1) N m U f G)
        (t : ℝ) :
        HasDerivAt (homogeneousPathFlux k N m G)
          (sphereFlux k (boundaryResidualFin
            (alphaPath (polynomialMap G) (coordinateMap (k+1)) m t)
            (betaLinear (polynomialMap G) (coordinateMap (k+1)) m))) t := by
    …

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