OAI/Geometry/NearbyLagrangian/MomentumSeparation.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Separation of branches by sphere and base momenta.

  1. theorem OAI.NearbyLagrangian.BranchSeparation.sub_mem_radial_of_sphere_momenta line 16
  2. theorem OAI.NearbyLagrangian.BranchSeparation.base_momentum_bound line 36
  3. theorem OAI.NearbyLagrangian.BranchSeparation.eq_of_equal_base_momenta line 47
  4. theorem OAI.NearbyLagrangian.BranchSeparation.exponential_differential_dominates line 72
  5. theorem OAI.NearbyLagrangian.MomentumCalculus.uncut_mfderiv line 93
  6. def OAI.NearbyLagrangian.MixedDerivative.baseDerivative line 131
  7. theorem OAI.NearbyLagrangian.MixedDerivative.contDiffAt_baseDerivative line 135
  8. theorem OAI.NearbyLagrangian.MixedDerivative.contMDiffAt_param_deriv line 162
  9. theorem OAI.NearbyLagrangian.MixedDerivative.contMDiffAt_param_fderiv line 173