Rename some lemmas to match mathlib4 convention better:

- is_holonomic_uncurry -> isHolonomicAt_uncurry
This lemma is about the predicate isHolonomicAt.
- one_jet_bundle_proj_continuous -> oneJetBundle_proj_continuous
- trivializationAt_one_jet_bundle_{source,target} -> trivializationAt_oneJetBundle_{source,target}
- smooth_one_jet_bundle_proj -> smooth_oneJetBundle_proj
- one_jet_bundle_mk_{fst,snd} -> oneJetBundle_mk_{fst,snd}
Not to be confused with OneJetBundle.mk, but this is clearly about
one-jet bundles.

Tweak one porting note.

SphereEversion/Global/Gromov.lean

@@ -141,7 +141,7 @@ theorem RelMfld.Ample.satisfiesHPrinciple' (hRample : R.Ample) (hRopen : IsOpen
     have η_cont : Continuous η := by
       have : ContMDiff IM ((IM.prod IX).prod 𝓘(ℝ, EM →L[ℝ] EX)) ∞ f := fun x ↦ hf_smooth x
       apply τ_cont.sub
-      exact (one_jet_bundle_proj_continuous.comp this.continuous).snd.dist 𝓕₀.smooth_bs.continuous
+      exact (oneJetBundle_proj_continuous.comp this.continuous).snd.dist 𝓕₀.smooth_bs.continuous
     rcases φ.improve_formalSol ψ hRample hRopen (hA.union C_closed) η_pos η_cont hFφψ hFAC K₀_cpct
         K₁_cpct K₀K₁' with
       ⟨F', hF'₀, hF'₁, hF'AC, hF'K₁, hF'η, hF'hol⟩
@@ -297,7 +297,7 @@ theorem RelMfld.Ample.satisfiesHPrinciple (hRample : R.Ample) (hRopen : IsOpen R
     have η_cont : Continuous η := by
       have : ContMDiff IM ((IM.prod IX).prod 𝓘(ℝ, EM →L[ℝ] EX)) ∞ f := fun x ↦ hf_smooth x
       apply τ_cont.sub
-      exact (one_jet_bundle_proj_continuous.comp this.continuous).snd.dist 𝓕₀.smooth_bs.continuous
+      exact (oneJetBundle_proj_continuous.comp this.continuous).snd.dist 𝓕₀.smooth_bs.continuous
     rcases(L.φ i).improve_formalSol (L.ψj i) hRample hRopen (hA.union hC) η_pos η_cont hFφψ hFAC hK₀
         hK₁ hK₀K₁ with
       ⟨F', hF'₀, hF'₁, hF'AC, hF'K₁, hF'η, hF'hol⟩

SphereEversion/Global/OneJetBundle.lean

@@ -178,7 +178,7 @@ end OneJetBundleInstances
 variable {I M I' M' J J'}
 
 /-- The tangent bundle projection on the basis is a continuous map. -/
-theorem one_jet_bundle_proj_continuous : Continuous (π (E →L[𝕜] E') FJ¹MM') :=
+theorem oneJetBundle_proj_continuous : Continuous (π (E →L[𝕜] E') FJ¹MM') :=
   FiberBundle.continuous_proj (E →L[𝕜] E') FJ¹MM'
 
 -- Porting note: removed next line
@@ -196,13 +196,13 @@ theorem oneJetBundle_trivializationAt (x₀ x : J¹MM') :
     Trivialization.pullback_symmL ContMDiffMap.fst (trivializationAt E (TangentSpace I) x₀.1.1)
       x.proj
 
-theorem trivializationAt_one_jet_bundle_source (x₀ : M × M') :
+theorem trivializationAt_oneJetBundle_source (x₀ : M × M') :
     (trivializationAt (E →L[𝕜] E') FJ¹MM' x₀).source =
       π (E →L[𝕜] E') FJ¹MM' ⁻¹'
         (Prod.fst ⁻¹' (chartAt H x₀.1).source ∩ Prod.snd ⁻¹' (chartAt H' x₀.2).source) :=
   rfl
 
-theorem trivializationAt_one_jet_bundle_target (x₀ : M × M') :
+theorem trivializationAt_oneJetBundle_target (x₀ : M × M') :
     (trivializationAt (E →L[𝕜] E') FJ¹MM' x₀).target =
       (Prod.fst ⁻¹' (trivializationAt E (TangentSpace I) x₀.1).baseSet ∩
           Prod.snd ⁻¹' (trivializationAt E' (TangentSpace I') x₀.2).baseSet) ×ˢ
@@ -226,7 +226,7 @@ theorem oneJetBundle_chart_source (x₀ : J¹MM') :
     (chartAt HJ x₀).source =
       π (E →L[𝕜] E') FJ¹MM' ⁻¹' (chartAt (ModelProd H H') x₀.proj).source := by
   -- Porting note: was
-  -- simp only [FiberBundle.chartedSpace_chartAt, trivializationAt_one_jet_bundle_source, mfld_simps]
+  -- simp only [FiberBundle.chartedSpace_chartAt, trivializationAt_oneJetBundle_source, mfld_simps]
   rw [FiberBundle.chartedSpace_chartAt]
   simp_rw [
     PartialHomeomorph.trans_toPartialEquiv,
@@ -239,14 +239,14 @@ theorem oneJetBundle_chart_source (x₀ : J¹MM') :
     PartialEquiv.refl_source,
     prodChartedSpace_chartAt,
     PartialHomeomorph.prod_toPartialEquiv,
-    trivializationAt_one_jet_bundle_source,
+    trivializationAt_oneJetBundle_source,
     PartialEquiv.prod_source,
     Set.preimage_inter]
   simp_rw [prod_univ, ← preimage_inter, ← Set.prod_eq, preimage_preimage, inter_eq_left,
     subset_def, mem_preimage]
   intro x hx
   rwa [Trivialization.coe_fst]
-  rwa [trivializationAt_one_jet_bundle_source, mem_preimage, ← Set.prod_eq]
+  rwa [trivializationAt_oneJetBundle_source, mem_preimage, ← Set.prod_eq]
 
 attribute [pp_dot] PartialEquiv.target PartialEquiv.symm PartialEquiv.prod
 
@@ -325,31 +325,31 @@ theorem oneJetBundle_chart_target (x₀ : J¹MM') :
 
 section Maps
 
-theorem smooth_one_jet_bundle_proj :
+theorem smooth_oneJetBundle_proj :
     Smooth ((I.prod I').prod 𝓘(𝕜, E →L[𝕜] E')) (I.prod I') (π (E →L[𝕜] E') FJ¹MM') := by
   apply smooth_proj _
 
 theorem Smooth.oneJetBundle_proj {f : N → J¹MM'}
     (hf : Smooth J ((I.prod I').prod 𝓘(𝕜, E →L[𝕜] E')) f) : Smooth J (I.prod I') fun x ↦ (f x).1 :=
-  smooth_one_jet_bundle_proj.comp hf
+  smooth_oneJetBundle_proj.comp hf
 
 theorem SmoothAt.oneJetBundle_proj {f : N → J¹MM'} {x₀ : N}
     (hf : SmoothAt J ((I.prod I').prod 𝓘(𝕜, E →L[𝕜] E')) f x₀) :
     SmoothAt J (I.prod I') (fun x ↦ (f x).1) x₀ :=
-  (smooth_one_jet_bundle_proj _).comp x₀ hf
+  (smooth_oneJetBundle_proj _).comp x₀ hf
 
 /-- The constructor of `OneJetBundle`, in case `Sigma.mk` will not give the right type. -/
 @[simp]
 def OneJetBundle.mk (x : M) (y : M') (f : OneJetSpace I I' (x, y)) : J¹MM' :=
   ⟨(x, y), f⟩
 
 @[simp, mfld_simps]
-theorem one_jet_bundle_mk_fst {x : M} {y : M'} {f : OneJetSpace I I' (x, y)} :
+theorem oneJetBundle_mk_fst {x : M} {y : M'} {f : OneJetSpace I I' (x, y)} :
     (OneJetBundle.mk x y f).1 = (x, y) :=
   rfl
 
 @[simp, mfld_simps]
-theorem one_jet_bundle_mk_snd {x : M} {y : M'} {f : OneJetSpace I I' (x, y)} :
+theorem oneJetBundle_mk_snd {x : M} {y : M'} {f : OneJetSpace I I' (x, y)} :
     (OneJetBundle.mk x y f).2 = f :=
   rfl
 
@@ -523,7 +523,7 @@ def mapLeft (f : M → N) (Dfinv : ∀ x : M, TangentSpace J (f x) →L[𝕜] Ta
 
 theorem mapLeft_eq_map (f : M → N) (Dfinv : ∀ x : M, TangentSpace J (f x) →L[𝕜] TangentSpace I x) :
     mapLeft f Dfinv = OneJetBundle.map I' I' f (id : M' → M') Dfinv := by
-  ext x; rfl; rfl; dsimp only [OneJetBundle.map, mapLeft, one_jet_bundle_mk_snd]
+  ext x; rfl; rfl; dsimp only [OneJetBundle.map, mapLeft, oneJetBundle_mk_snd]
   simp_rw [mfderiv_id, ContinuousLinearMap.id_comp]
 
 theorem SmoothAt.mapLeft {f : N' → M → N} {x₀ : N'}
@@ -562,9 +562,9 @@ theorem smooth_bundleSnd :
     ContMDiffAt.mfderiv (fun (x : OneJetBundle (J.prod I) (N × M) I' M') (y : M) ↦ (x.1.1.1, y))
       (fun x : OneJetBundle (J.prod I) (N × M) I' M' ↦ x.1.1.2) ?_ ?_ le_top
   exact this
-  · exact (smooth_one_jet_bundle_proj.fst.fst.prod_map smooth_id).smoothAt
+  · exact (smooth_oneJetBundle_proj.fst.fst.prod_map smooth_id).smoothAt
   -- slow
-  · exact smooth_one_jet_bundle_proj.fst.snd.smoothAt
+  · exact smooth_oneJetBundle_proj.fst.snd.smoothAt
 
 -- slow
 end Maps
@@ -618,7 +618,7 @@ variable (I I')
 
 -- note: this proof works for all vector bundles where we have proven
 -- `∀ p, chartAt _ p = f.toPartialEquiv`
-/-- The canonical identification between the one_jet bundle to the model space and the product,
+/-- The canonical identification between the one-jet bundle to the model space and the product,
 as a homeomorphism -/
 def oneJetBundleModelSpaceHomeomorph : OneJetBundle I H I' H' ≃ₜ 𝓜 :=
   { Bundle.TotalSpace.toProd (H × H') (E →L[𝕜] E') with

SphereEversion/Global/OneJetSec.lean

@@ -94,7 +94,7 @@ theorem smooth_eta (F : OneJetSec I M I' M') :
   F.smooth
 
 theorem smooth_bs (F : OneJetSec I M I' M') : Smooth I I' F.bs :=
-  smooth_one_jet_bundle_proj.snd.comp F.smooth
+  smooth_oneJetBundle_proj.snd.comp F.smooth
 
 /-- A section of J¹(M, M') is holonomic at (x : M) if its linear map part is the derivative
 of its base map at x. -/
@@ -106,7 +106,7 @@ its base map at x. -/
 theorem isHolonomicAt_iff {F : OneJetSec I M I' M'} {x : M} :
     F.IsHolonomicAt x ↔ oneJetExt I I' F.bs x = F x := by
   simp_rw [IsHolonomicAt, oneJetExt, Bundle.TotalSpace.ext_iff, heq_iff_eq, F.fst_eq,
-    one_jet_bundle_mk_fst, true_and_iff, one_jet_bundle_mk_snd]
+    oneJetBundle_mk_fst, true_and_iff, oneJetBundle_mk_snd]
 
 theorem isHolonomicAt_congr {F F' : OneJetSec I M I' M'} {x : M} (h : F =ᶠ[𝓝 x] F') :
     F.IsHolonomicAt x ↔ F'.IsHolonomicAt x := by
@@ -223,7 +223,7 @@ protected theorem smooth (S : FamilyOneJetSec I M I' M' J N) :
 
 theorem smooth_bs (S : FamilyOneJetSec I M I' M' J N) :
     Smooth (J.prod I) I' fun p : N × M ↦ S.bs p.1 p.2 :=
-  smooth_one_jet_bundle_proj.snd.comp S.smooth
+  smooth_oneJetBundle_proj.snd.comp S.smooth
 
 theorem smooth_coe_bs (S : FamilyOneJetSec I M I' M' J N) {p : N} : Smooth I I' (S.bs p) :=
   (S p).smooth_bs
@@ -267,7 +267,7 @@ theorem uncurry_ϕ' (S : FamilyOneJetSec I M I' M' IP P) (p : P × M) :
   simp_rw [mfderiv_fst]
   rfl
 
-theorem is_holonomic_uncurry (S : FamilyOneJetSec I M I' M' IP P) {p : P × M} :
+theorem isHolonomicAt_uncurry (S : FamilyOneJetSec I M I' M' IP P) {p : P × M} :
     S.uncurry.IsHolonomicAt p ↔ (S p.1).IsHolonomicAt p.2 := by
   simp_rw [OneJetSec.IsHolonomicAt, OneJetSec.snd_eq, S.uncurry_ϕ]
   rw [show S.uncurry.bs = fun x ↦ S.uncurry.bs x from rfl, funext S.uncurry_bs]

SphereEversion/Global/ParametricityForFree.lean

@@ -95,7 +95,7 @@ theorem relativize_slice {σ : OneJetBundle (IP.prod I) (P × M) I' M'}
     (show Set E' from R.slice (bundleSnd σ) q)
   dsimp only at this
   erw [← this, mem_preimage, mem_slice, R.mem_relativize]
-  dsimp only [one_jet_bundle_mk_fst, one_jet_bundle_mk_snd]
+  dsimp only [oneJetBundle_mk_fst, oneJetBundle_mk_snd]
   congr!
 
 theorem relativize_slice_eq_univ {σ : OneJetBundle (IP.prod I) (P × M) I' M'}
@@ -120,7 +120,7 @@ theorem relativize_slice_eq_univ {σ : OneJetBundle (IP.prod I) (P × M) I' M'}
   conv_rhs =>
     ext
     erw [mem_slice, R.mem_relativize, this]
-  dsimp only [one_jet_bundle_mk_fst, one_jet_bundle_mk_snd]
+  dsimp only [oneJetBundle_mk_fst, oneJetBundle_mk_snd]
   simp [this, exists_const, forall_const]
 
 variable (IP P)
@@ -265,7 +265,7 @@ theorem RelMfld.SatisfiesHPrinciple.satisfiesHPrincipleWith (R : RelMfld I M IX
     R.SatisfiesHPrincipleWith IP C ε := by
   intro 𝓕₀ h𝓕₀
   obtain ⟨𝓕, h1𝓕, h2𝓕, h3𝓕, h4𝓕⟩ :=
-    h 𝓕₀.uncurry (h𝓕₀.mono fun p hp => 𝓕₀.toFamilyOneJetSec.is_holonomic_uncurry.mpr hp)
+    h 𝓕₀.uncurry (h𝓕₀.mono fun p hp => 𝓕₀.toFamilyOneJetSec.isHolonomicAt_uncurry.mpr hp)
   refine' ⟨𝓕.curry, _, _, _, _⟩
   · intro s x; exact curry_eq_iff_eq_uncurry (h1𝓕 (s, x))
   · intro s x; exact 𝓕.toFamilyOneJetSec.isHolonomicAt_curry (h2𝓕 (s, x))

SphereEversion/Global/Relation.lean

@@ -189,7 +189,7 @@ theorem slice_mk_update {R : RelMfld I M I' M'} {σ : OneJetBundle I M I' M'}
   rw [mem_slice]
   change _ ↔ OneJetBundle.mk σ.proj.1 σ.proj.2 (DualPair.update p σ.snd w) ∈ R
   convert Iff.rfl using 3
-  rw [one_jet_bundle_mk_snd, p.update_update]
+  rw [oneJetBundle_mk_snd, p.update_update]
 
 /-- A differential relation is ample if all its slices are ample sets. -/
 def RelMfld.Ample (R : RelMfld I M I' M') : Prop :=
@@ -476,7 +476,7 @@ theorem OpenSmoothEmbedding.smooth_transfer :
   have' :=
     ContMDiffAt.mfderiv (fun _ => φ.invFun) (fun x : OneJetBundle IX X IY Y => φ x.1.1)
       ((φ.smoothAt_inv <| _).comp (x, φ x.1.1) smoothAt_snd)
-      (φ.smooth_to.smoothAt.comp x (smooth_one_jet_bundle_proj.fst x)) le_top
+      (φ.smooth_to.smoothAt.comp x (smooth_oneJetBundle_proj.fst x)) le_top
   · simp_rw [φ.left_inv] at this ; exact this
   exact mem_range_self _
 
@@ -495,11 +495,10 @@ theorem OpenSmoothEmbedding.range_transfer :
       ⟨⟨(x, y), ((ψ.fderiv y).symm : TangentSpace IN (ψ y) →L[ℝ] TangentSpace IY y) ∘L
             τ ∘L (φ.fderiv x : TangentSpace IX x →L[ℝ] TangentSpace IM (φ x))⟩, ?_⟩
     refine congr_arg (Bundle.TotalSpace.mk _) (ContinuousLinearMap.ext fun v ↦ ?_)
+    dsimp only [OpenSmoothEmbedding.transfer, OneJetBundle.map, OneJetBundle.mk]
     /- Porting note: Lean 3 version was
-    dsimp only [open_smooth_embedding.transfer, one_jet_bundle.map, one_jet_bundle.mk],
     simp_rw [continuous_linear_map.comp_apply, ← ψ.fderiv_coe, continuous_linear_equiv.coe_coe,
       (φ.fderiv x).apply_symm_apply, (ψ.fderiv y).apply_symm_apply] -/
-    dsimp only [OpenSmoothEmbedding.transfer, OneJetBundle.map, OneJetBundle.mk]
     simp only [ContinuousLinearMap.comp_apply, ← ψ.fderiv_coe]
     erw [ContinuousLinearEquiv.coe_coe (fderiv ψ  y), (ψ.fderiv y).apply_symm_apply]
     change τ _ = _
@@ -508,7 +507,7 @@ theorem OpenSmoothEmbedding.range_transfer :
 
 theorem OpenSmoothEmbedding.isOpen_range_transfer : IsOpen (range (φ.transfer ψ)) := by
   rw [φ.range_transfer ψ]
-  exact (φ.isOpen_range.prod ψ.isOpen_range).preimage one_jet_bundle_proj_continuous
+  exact (φ.isOpen_range.prod ψ.isOpen_range).preimage oneJetBundle_proj_continuous
 
 /-- localize a relation -/
 def RelMfld.localize (R : RelMfld IM M IN N) : RelMfld IX X IY Y :=
@@ -532,8 +531,8 @@ theorem RelMfld.Ample.localize (hR : R.Ample) : (R.localize φ ψ).Ample := by
       mem_slice, mem_preimage]
     -- Porting note: the next `rw` should be part of the `simp_rw` above
     rw [mem_slice]
-    dsimp only [OpenSmoothEmbedding.transfer, OneJetBundle.map, one_jet_bundle_mk_fst,
-      one_jet_bundle_mk_snd]
+    dsimp only [OpenSmoothEmbedding.transfer, OneJetBundle.map, oneJetBundle_mk_fst,
+      oneJetBundle_mk_snd]
     -- Porting note: the next `rw` should be part of the `simp_rw` below
     rw [p.map_update_comp_right, ← p.update_comp_left]
     simp_rw [OneJetBundle.mk, ← ψ.fderiv_coe]
@@ -642,7 +641,7 @@ def OneJetBundle.embedding : OpenSmoothEmbedding IXY J¹XY IMN J¹MN
     have' :=
       ContMDiffAt.mfderiv (fun _ => φ) (fun x : OneJetBundle IM M IN N => φ.invFun x.1.1)
         (φ.smooth_to.smoothAt.comp _ smoothAt_snd)
-        ((φ.smoothAt_inv _).comp _ (smooth_one_jet_bundle_proj.fst (φ.transfer ψ x))) le_top
+        ((φ.smoothAt_inv _).comp _ (smooth_oneJetBundle_proj.fst (φ.transfer ψ x))) le_top
     · dsimp only [id]
       refine' this.congr_of_eventuallyEq _
       refine' Filter.eventually_of_mem ((φ.isOpen_range_transfer ψ).mem_nhds (mem_range_self _)) _

SphereEversion/Global/TwistOneJetSec.lean

@@ -32,7 +32,7 @@ notation "J¹[" 𝕜 ", " E ", " I ", " M ", " V "]" => TotalSpace (E →L[𝕜]
 variable {I M V}
 variable {f : N → J¹[𝕜, E, I, M, V]}
 
--- todo: remove or use to prove `smooth_at_one_jet_eucl_bundle`
+-- todo: remove or use to prove `smoothAt_one_jet_eucl_bundle`
 theorem smoothAt_one_jet_eucl_bundle' {x₀ : N} :
     SmoothAt J (I.prod 𝓘(𝕜, E →L[𝕜] V)) f x₀ ↔ SmoothAt J I (fun x  ↦ (f x).1) x₀ ∧
     SmoothAt J 𝓘(𝕜, E →L[𝕜] V) (fun x  ↦ show E →L[𝕜] V from

blueprint/src/global_convex_integration.tex

@@ -496,7 +496,7 @@ \subsection*{Parametricity for free}
   \label{lem:param_trick}
   \uses{def:holonomic_section, def:formal_sol}
   \leanok
-  \lean{FamilyOneJetSec.is_holonomic_uncurry, FamilyOneJetSec.uncurry_mem_relativize}
+  \lean{FamilyOneJetSec.isHolonomicAt_uncurry, FamilyOneJetSec.uncurry_mem_relativize}
   In the above setup, we have:
   \begin{itemize}
     \item