import Mathlib/-! Area-controlled end replacement and Schwarzschild equality examples. -/namespace OAI.CKSADMend OAI.CKSADMnamespace OAI.CKSAngularGeometryend OAI.CKSAngularGeometrynamespace OAI.CKSAngularSliceend OAI.CKSAngularSlicenamespace OAI.CKSBoundarySurfaceend OAI.CKSBoundarySurfacenamespace OAI.CKSCalculusend OAI.CKSCalculusnamespace OAI.CKSCartesianOuterend OAI.CKSCartesianOuternamespace OAI.CKSEmbeddingDerivativeend OAI.CKSEmbeddingDerivativenamespace OAI.CKSFullCutAreaend OAI.CKSFullCutAreanamespace OAI.CKSGeometricCutsend OAI.CKSGeometricCutsnamespace OAI.CKSInducedAreaend OAI.CKSInducedAreanamespace OAI.CKSInducedSphereend OAI.CKSInducedSpherenamespace OAI.CKSIntrinsicConstraintsend OAI.CKSIntrinsicConstraintsnamespace OAI.CKSIntrinsicGeometryend OAI.CKSIntrinsicGeometrynamespace OAI.CKSIntrinsicVolumeend OAI.CKSIntrinsicVolumenamespace OAI.CKSLocalBendingend OAI.CKSLocalBendingnamespace OAI.CKSLorentzend OAI.CKSLorentznamespace OAI.CKSLorentz.SmoothAngularPatchend OAI.CKSLorentz.SmoothAngularPatchnamespace OAI.CKSMainend OAI.CKSMainnamespace OAI.CKSMain.InteriorSurfaceend OAI.CKSMain.InteriorSurfacenamespace OAI.CKSMetricGluingend OAI.CKSMetricGluingnamespace OAI.CKSMixedGeometryend OAI.CKSMixedGeometrynamespace OAI.CKSMixedGeometry.FiniteLogDecayend OAI.CKSMixedGeometry.FiniteLogDecaynamespace OAI.CKSRealizedRoundend OAI.CKSRealizedRoundnamespace OAI.CKSReplacementCompletenessend OAI.CKSReplacementCompletenessnamespace OAI.CKSRoundend OAI.CKSRoundnamespace OAI.CKSRound.MetricJetend OAI.CKSRound.MetricJetnamespace OAI.CKSSchwarzschildend OAI.CKSSchwarzschildnamespace OAI.CKSSourceExteriorend OAI.CKSSourceExteriornamespace OAI.CKSSpatialManifoldend OAI.CKSSpatialManifoldnamespace OAI.CKSSphericalHarmonicsend OAI.CKSSphericalHarmonicsnamespace OAI.CKSSurfaceVolumeend OAI.CKSSurfaceVolumenoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSSpatialManifoldlocal instance real_id_isometric : RingHomIsometric (RingHom.id ℝ) := inferInstanceend OAI.CKSSpatialManifoldendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSMetricGluingopen Bundle Manifold Set Bornologyopen scoped Bundle Manifold ContDiffvariable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type*} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type*} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I ∞ M]local instance real_continuousAdd : ContinuousAdd ℝ := inferInstancelocal instance real_continuousConstSMul : ContinuousConstSMul ℝ ℝ := inferInstancelocal instance real_smulCommClass : @SMulCommClass ℝ ℝ ℝ Algebra.toSMul (@instSMulOfMul ℝ (@Distrib.toMul ℝ (@instDistribOfSemiring ℝ (@CommSemiring.toSemiring ℝ Real.instCommSemiring)))) := inferInstanceend OAI.CKSMetricGluingendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSMetricGluingopen Bundle Manifold Set Bornologyopen scoped Bundle Manifold ContDiffvariable {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I ∞ M]attribute [local instance] real_continuousAddabbrev InnerField := letI := OAI.CKSMetricGluing.real_smulCommClass letI := OAI.CKSMetricGluing.real_continuousConstSMul ∀ x : M, TangentSpace I x →L[ℝ] TangentSpace I x →L[ℝ] ℝabbrev SmoothMetric := ContMDiffRiemannianMetric I ∞ E (fun x : M => TangentSpace I x)def innerSection (q : OAI.CKSMetricGluing.InnerField I (M := M)) : M → TotalSpace (E →L[ℝ] E →L[ℝ] ℝ) (fun x : M => TangentSpace I x →L[ℝ] TangentSpace I x →L[ℝ] ℝ) := fun x => ⟨x,q x⟩end OAI.CKSMetricGluingendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSAngularGeometryopen Set Filteropen scoped Topology ContDiff NNReal Matrix.Norms.Elementwiseabbrev I := Fin 2end OAI.CKSAngularGeometryendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSCalculusopen Filter Setopen scoped Topology ContDiffvariable {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E]def D (e : E) (f : E → ℝ) (x : E) : ℝ := fderiv ℝ f x eend OAI.CKSCalculusendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSRoundabbrev Idx := Fin 3abbrev Mat := Matrix OAI.CKSRound.Idx OAI.CKSRound.Idx ℝstructure MetricJet where inv : OAI.CKSRound.Mat d : OAI.CKSRound.Idx → OAI.CKSRound.Mat dd : OAI.CKSRound.Idx → OAI.CKSRound.Idx → OAI.CKSRound.Matend OAI.CKSRoundendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSRound.MetricJetdef gamma (j : OAI.CKSRound.MetricJet) (a i k : OAI.CKSRound.Idx) : ℝ := (∑ l, j.inv a l * (j.d i k l + j.d k i l - j.d l i k)) / 2def dInv (j : OAI.CKSRound.MetricJet) (s a b : OAI.CKSRound.Idx) : ℝ := - ∑ i, ∑ k, j.inv a i * j.d s i k * j.inv k bdef dGamma (j : OAI.CKSRound.MetricJet) (s a i k : OAI.CKSRound.Idx) : ℝ := (∑ l, (j.dInv s a l * (j.d i k l + j.d k i l - j.d l i k) + j.inv a l * (j.dd s i k l + j.dd s k i l - j.dd s l i k))) / 2def ricci (j : OAI.CKSRound.MetricJet) (i k : OAI.CKSRound.Idx) : ℝ := (∑ a, (j.dGamma a a i k - j.dGamma k a i a)) + ∑ a, ∑ b, (j.gamma a a b * j.gamma b i k - j.gamma a k b * j.gamma b i a)def scalar (j : OAI.CKSRound.MetricJet) : ℝ := ∑ i, ∑ k, j.inv i k * j.ricci i kend OAI.CKSRound.MetricJetendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSRoundstructure TensorJet where val : OAI.CKSRound.Mat d : OAI.CKSRound.Idx → OAI.CKSRound.Matend OAI.CKSRoundendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSRound.MetricJetdef trace (g : OAI.CKSRound.MetricJet) (k : OAI.CKSRound.TensorJet) : ℝ := ∑ a, ∑ b, g.inv a b * k.val a bdef normSq (g : OAI.CKSRound.MetricJet) (k : OAI.CKSRound.TensorJet) : ℝ := ∑ a, ∑ b, ∑ c, ∑ d, g.inv a c * g.inv b d * k.val a b * k.val c ddef dTrace (g : OAI.CKSRound.MetricJet) (k : OAI.CKSRound.TensorJet) (i : OAI.CKSRound.Idx) : ℝ := ∑ a, ∑ b, (g.dInv i a b * k.val a b + g.inv a b * k.d i a b)def tensorDivergence (g : OAI.CKSRound.MetricJet) (k : OAI.CKSRound.TensorJet) (i : OAI.CKSRound.Idx) : ℝ := ∑ a, ∑ b, g.inv a b * (k.d a b i - (∑ c, g.gamma c a b * k.val c i) - (∑ c, g.gamma c a i * k.val b c))def energy (g : OAI.CKSRound.MetricJet) (k : OAI.CKSRound.TensorJet) : ℝ := (g.scalar + g.trace k ^ 2 - g.normSq k) / 2def momentum (g : OAI.CKSRound.MetricJet) (k : OAI.CKSRound.TensorJet) (i : OAI.CKSRound.Idx) : ℝ := g.tensorDivergence k i - g.dTrace k iend OAI.CKSRound.MetricJetendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSRealizedRoundopen CKSCalculus CKSRoundopen scoped Topology ContDiffabbrev Point := Fin 3 → ℝdef basis (a : OAI.CKSRound.Idx) : OAI.CKSRealizedRound.Point := Pi.single a 1end OAI.CKSRealizedRoundendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSLocalBendingopen CKSRounddef momentumSq (j : OAI.CKSRound.MetricJet) (k : OAI.CKSRound.TensorJet) : ℝ := ∑ i, ∑ l, j.inv i l * j.momentum k i * j.momentum k ldef DEC (j : OAI.CKSRound.MetricJet) (k : OAI.CKSRound.TensorJet) : Prop := Real.sqrt (OAI.CKSLocalBending.momentumSq j k) ≤ j.energy kend OAI.CKSLocalBendingendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSAngularGeometryopen CKSCalculus Set Filteropen scoped Topology ContDiff NNReal Matrix.Norms.Elementwiseabbrev Point := OAI.CKSAngularGeometry.I → ℝdef basis (a : OAI.CKSAngularGeometry.I) : OAI.CKSAngularGeometry.Point := Pi.single a 1end OAI.CKSAngularGeometryendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSAngularGeometryopen CKSCalculus Set Filter Matrixopen scoped Topology ContDiff NNReal Matrix.Norms.Elementwiseabbrev AmbientMat := Matrix (Fin 3) (Fin 3) ℝend OAI.CKSAngularGeometryendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSAngularGeometryopen Matrix CKSCalculusopen scoped BigOperatorsabbrev PhysicalPoint := Fin 3 → ℝend OAI.CKSAngularGeometryendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSMixedGeometryopen CKSCalculus Set Filteropen scoped Topology ContDiff NNReal Matrix.Norms.Elementwiseabbrev I := Fin 3abbrev A := Fin 2abbrev Point := OAI.CKSMixedGeometry.I → ℝdef basis (a : OAI.CKSMixedGeometry.I) : OAI.CKSMixedGeometry.Point := Pi.single a 1end OAI.CKSMixedGeometryendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSMixedGeometryopen CKSCalculus Set Filteropen scoped Topology ContDiff NNReallocal instance pointDimension_neZero : NeZero (3 : ℕ) := inferInstancedef radialFactor (a : OAI.CKSMixedGeometry.I) (y : OAI.CKSMixedGeometry.Point) : ℝ := letI := OAI.CKSMixedGeometry.pointDimension_neZero if a = 0 then y 0 else 1def scaledD (a : OAI.CKSMixedGeometry.I) (f : OAI.CKSMixedGeometry.Point → ℝ) : OAI.CKSMixedGeometry.Point → ℝ := fun y => OAI.CKSMixedGeometry.radialFactor a y * OAI.CKSCalculus.D (OAI.CKSMixedGeometry.basis a) f ydef scaledIter : List OAI.CKSMixedGeometry.I → (OAI.CKSMixedGeometry.Point → ℝ) → OAI.CKSMixedGeometry.Point → ℝ | [], f => f | a::l,f => OAI.CKSMixedGeometry.scaledD a (scaledIter l f)end OAI.CKSMixedGeometryendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSMixedGeometryopen CKSCalculus Set Filteropen scoped Topology ContDiff NNReal Matrix.Norms.Elementwiseabbrev Angle := OAI.CKSMixedGeometry.A → ℝdef angularProjection : OAI.CKSMixedGeometry.Point →L[ℝ] OAI.CKSMixedGeometry.Angle := ContinuousLinearMap.pi (fun a => ContinuousLinearMap.proj a.succ)def ScaledComponentBound (f : OAI.CKSMixedGeometry.Point → ℝ) (j q : ℕ) (B : ℝ) (y : OAI.CKSMixedGeometry.Point) : Prop := letI := OAI.CKSMixedGeometry.pointDimension_neZero ∀ l : List OAI.CKSMixedGeometry.I, l.length ≤ j → |scaledIter l f y| ≤ B/(y 0)^qend OAI.CKSMixedGeometryendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSInducedSphereopen Finsetabbrev Ix := Fin 3end OAI.CKSInducedSphereendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSSphericalHarmonicsopen MvPolynomialabbrev Ambient := EuclideanSpace ℝ (Fin 3)abbrev Sphere := ↥(Metric.sphere (0 : OAI.CKSSphericalHarmonics.Ambient) 1)end OAI.CKSSphericalHarmonicsendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSSphericalHarmonicsopen MvPolynomialopen MeasureTheoryabbrev surfaceMeasure : Measure OAI.CKSSphericalHarmonics.Sphere := (volume : Measure OAI.CKSSphericalHarmonics.Ambient).toSphereend OAI.CKSSphericalHarmonicsendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSSphericalHarmonicsopen MvPolynomialopen MeasureTheoryopen scoped Pointwiseopen scoped Manifold ContDiff Topologyopen Setdef SmoothSphere (f : OAI.CKSSphericalHarmonics.Sphere → ℝ) : Prop := ContMDiff (𝓡 2) 𝓘(ℝ, ℝ) ∞ fend OAI.CKSSphericalHarmonicsendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSLorentzlocal instance two_atLeastTwo : Nat.AtLeastTwo 2 := inferInstanceend OAI.CKSLorentzendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSInducedSphereopen Set Filter Finsetopen scoped Topology ContDiffabbrev E := EuclideanSpace ℝ OAI.CKSInducedSphere.Ixend OAI.CKSInducedSphereendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSInducedSphereopen Set Filter Finsetopen scoped Topology ContDiffattribute [local instance] CKSLorentz.two_atLeastTwodef e (i : OAI.CKSInducedSphere.Ix) : OAI.CKSInducedSphere.E := WithLp.toLp 2 (Pi.single i 1)def pd (i : OAI.CKSInducedSphere.Ix) (F : OAI.CKSInducedSphere.E → ℝ) (x : OAI.CKSInducedSphere.E) : ℝ := fderiv ℝ F x (OAI.CKSInducedSphere.e i)end OAI.CKSInducedSphereendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSLorentzopen scoped InnerProductSpace RealInnerProductSpace ContDiff Manifold Topologyopen Setabbrev E := EuclideanSpace ℝ (Fin 3)abbrev V := ℝ × OAI.CKSLorentz.Eabbrev Sphere := ↥(Metric.sphere (0 : OAI.CKSLorentz.E) 1)end OAI.CKSLorentzendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSLorentzopen CKSMixedGeometry CKSAngularSlice Setopen scoped ContDiff Topologylocal instance pointDimension_neZero : NeZero (3 : ℕ) := inferInstancedef ordinaryLeadingComponent (q : ℕ) (M : OAI.CKSMixedGeometry.Angle → ℝ) (y : OAI.CKSMixedGeometry.Point) : ℝ := letI := OAI.CKSLorentz.pointDimension_neZero 1/(y 0)^q * M (OAI.CKSMixedGeometry.angularProjection y)end OAI.CKSLorentzendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSMixedGeometryopen Setopen scoped ContDiffstructure SourceRemainderOn (j q : ℕ) (V : Set OAI.CKSMixedGeometry.Point) (f : OAI.CKSMixedGeometry.Point → ℝ) : Prop where regular : ∀ y ∈ V, ContDiffAt ℝ j f y bound : ∃ B : ℝ, 0 ≤ B ∧ ∀ y ∈ V, OAI.CKSMixedGeometry.ScaledComponentBound f j q B yend OAI.CKSMixedGeometryendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSLorentzopen CKSMixedGeometry CKSAngularSlice Setopen scoped ContDiff Topologystructure SourceCKSComponents (j qrad : ℕ) (V : Set OAI.CKSMixedGeometry.Point) (A : OAI.CKSMixedGeometry.I → OAI.CKSMixedGeometry.I → OAI.CKSMixedGeometry.Point → ℝ) (mr : OAI.CKSMixedGeometry.Angle → ℝ) (mg : OAI.CKSMixedGeometry.I → OAI.CKSMixedGeometry.I → OAI.CKSMixedGeometry.Angle → ℝ) : Prop where radial : OAI.CKSMixedGeometry.SourceRemainderOn j qrad V (fun y => A 0 0 y-OAI.CKSLorentz.ordinaryLeadingComponent 5 mr y) mixed : ∀ i k, (i=0 ∧ k≠0) ∨ (i≠0 ∧ k=0) → OAI.CKSMixedGeometry.SourceRemainderOn j 3 V (A i k) angular : ∀ i k, i≠0 → k≠0 → OAI.CKSMixedGeometry.SourceRemainderOn j 2 V (fun y => A i k y-OAI.CKSLorentz.ordinaryLeadingComponent 1 (mg i k) y)end OAI.CKSLorentzendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSLorentzopen CKSMixedGeometry CKSAngularSlice Setdef angularRadialTail (R : ℝ) (W : Set OAI.CKSMixedGeometry.Angle) : Set OAI.CKSMixedGeometry.Point := letI := OAI.CKSLorentz.pointDimension_neZero {y | R < y 0 ∧ OAI.CKSMixedGeometry.angularProjection y ∈ W}end OAI.CKSLorentzendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSLorentzopen CKSMixedGeometry CKSAngularSlice Setopen scoped ContDiff Topologystructure SmoothAngularPatch where chart : OpenPartialHomeomorph OAI.CKSLorentz.Sphere OAI.CKSMixedGeometry.Angle param_smooth : ContDiffOn ℝ ∞ (fun θ => (chart.symm θ : OAI.CKSLorentz.E)) chart.target extension : OAI.CKSLorentz.E → OAI.CKSMixedGeometry.Angle domain : Set OAI.CKSLorentz.E isOpen_domain : IsOpen domain extension_smooth : ContDiffOn ℝ ∞ extension domain source_domain : ∀ n ∈ chart.source, (n:OAI.CKSLorentz.E) ∈ domain extension_eq : ∀ n ∈ chart.source, extension n = chart nend OAI.CKSLorentzendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSLorentz.SmoothAngularPatchopen CKSMixedGeometry CKSAngularSlice Setopen scoped ContDiff Topologydef param (P : OAI.CKSLorentz.SmoothAngularPatch) (θ : OAI.CKSMixedGeometry.Angle) : OAI.CKSLorentz.E := P.chart.symm θdef sphereRegion (P : OAI.CKSLorentz.SmoothAngularPatch) (W : Set OAI.CKSMixedGeometry.Angle) : Set OAI.CKSLorentz.Sphere := P.chart.source ∩ P.chart ⁻¹' Wend OAI.CKSLorentz.SmoothAngularPatchendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSLorentzopen CKSMixedGeometry CKSAngularSlice Setopen scoped ContDiff Topologystructure CKSTensorPatch where patch : OAI.CKSLorentz.SmoothAngularPatch region : Set OAI.CKSMixedGeometry.Angle open_region : IsOpen region region_target : region ⊆ patch.chart.target radius : ℝ metric : OAI.CKSMixedGeometry.I → OAI.CKSMixedGeometry.I → OAI.CKSMixedGeometry.Point → ℝ second : OAI.CKSMixedGeometry.I → OAI.CKSMixedGeometry.I → OAI.CKSMixedGeometry.Point → ℝ mr : OAI.CKSMixedGeometry.Angle → ℝ mg : OAI.CKSMixedGeometry.I → OAI.CKSMixedGeometry.I → OAI.CKSMixedGeometry.Angle → ℝ mK : OAI.CKSMixedGeometry.I → OAI.CKSMixedGeometry.I → OAI.CKSMixedGeometry.Angle → ℝ mr_smooth : ContDiffOn ℝ ∞ mr region mg_smooth : ∀ i k, i≠0 → k≠0 → ContDiffOn ℝ ∞ (mg i k) region mK_smooth : ∀ i k, i≠0 → k≠0 → ContDiffOn ℝ ∞ (mK i k) region metric_CKS : OAI.CKSLorentz.SourceCKSComponents 3 6 (OAI.CKSLorentz.angularRadialTail radius region) metric mr mg second_CKS : OAI.CKSLorentz.SourceCKSComponents 2 5 (OAI.CKSLorentz.angularRadialTail radius region) second (fun _ => 0) mKend OAI.CKSLorentzendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSLorentzopen CKSMixedGeometry CKSAngularSlicelocal instance real_continuousAdd : ContinuousAdd ℝ := inferInstancelocal instance real_continuousConstSMul : ContinuousConstSMul ℝ ℝ := inferInstancelocal instance real_smulCommClass : @SMulCommClass ℝ ℝ ℝ Algebra.toSMul (@instSMulOfMul ℝ (@Distrib.toMul ℝ (@instDistribOfSemiring ℝ (@CommSemiring.toSemiring ℝ Real.instCommSemiring)))) := inferInstanceend OAI.CKSLorentzendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSLorentzopen CKSMixedGeometry CKSAngularSliceattribute [local instance] real_continuousAddabbrev SpatialBilinear := letI := OAI.CKSLorentz.real_smulCommClass letI := OAI.CKSLorentz.real_continuousConstSMul OAI.CKSLorentz.E →L[ℝ] OAI.CKSLorentz.E →L[ℝ] ℝabbrev SpatialTensor := OAI.CKSLorentz.E → OAI.CKSLorentz.SpatialBilinearlocal instance three_neZero : NeZero 3 := inferInstancedef polarParam (P : OAI.CKSLorentz.SmoothAngularPatch) (y : OAI.CKSMixedGeometry.Point) : OAI.CKSLorentz.E := letI := OAI.CKSLorentz.three_neZero y 0 • P.param (OAI.CKSMixedGeometry.angularProjection y)def polarTensorComponents (P : OAI.CKSLorentz.SmoothAngularPatch) (A : OAI.CKSLorentz.SpatialTensor) (i k : OAI.CKSMixedGeometry.I) (y : OAI.CKSMixedGeometry.Point) : ℝ := A (OAI.CKSLorentz.polarParam P y) (fderiv ℝ (OAI.CKSLorentz.polarParam P) y (OAI.CKSMixedGeometry.basis i)) (fderiv ℝ (OAI.CKSLorentz.polarParam P) y (OAI.CKSMixedGeometry.basis k))def CKSTensorPatch.Realizes (Q : OAI.CKSLorentz.CKSTensorPatch) (A B : OAI.CKSLorentz.SpatialTensor) : Prop := ∀ y ∈ OAI.CKSLorentz.angularRadialTail Q.radius Q.region, ∀ i k, Q.metric i k y = OAI.CKSLorentz.polarTensorComponents Q.patch A i k y ∧ Q.second i k y = OAI.CKSLorentz.polarTensorComponents Q.patch B i k yend OAI.CKSLorentzendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSLorentzopen CKSMixedGeometry CKSAngularSlice CKSCalculusabbrev AngularMatrix := Matrix (Fin 2) (Fin 2) ℝdef angularMetricTrace (σ A : OAI.CKSLorentz.AngularMatrix) : ℝ := (σ⁻¹ * A).tracedef angularRoundMetric (φ : OAI.CKSMixedGeometry.Angle → OAI.CKSLorentz.E) (θ : OAI.CKSMixedGeometry.Angle) : OAI.CKSLorentz.AngularMatrix := letI := OAI.CKSLorentz.two_atLeastTwo letI : Inner ℝ OAI.CKSLorentz.E := @InnerProductSpace.toInner ℝ OAI.CKSLorentz.E _ (PiLp.seminormedAddCommGroup 2 (fun _ : Fin 3 => ℝ)) (PiLp.innerProductSpace (fun _ : Fin 3 => ℝ)) fun a b => inner ℝ (fderiv ℝ φ θ (OAI.CKSAngularGeometry.basis a)) (fderiv ℝ φ θ (OAI.CKSAngularGeometry.basis b))end OAI.CKSLorentzendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSLorentzopen scoped RealInnerProductSpace ContDiff Manifold Topologyopen MeasureTheoryopen CKSSphericalHarmonics (SmoothSphere surfaceMeasure)def nullDirection (n : OAI.CKSLorentz.Sphere) : OAI.CKSLorentz.V := (1,(n:OAI.CKSLorentz.E))def rawCharge (M : OAI.CKSLorentz.Sphere → ℝ) : OAI.CKSLorentz.V := ∫ n : OAI.CKSLorentz.Sphere, M n • OAI.CKSLorentz.nullDirection n ∂OAI.CKSSphericalHarmonics.surfaceMeasuredef bondiCharge (M : OAI.CKSLorentz.Sphere → ℝ) : OAI.CKSLorentz.V := (16*Real.pi)⁻¹ • OAI.CKSLorentz.rawCharge Mend OAI.CKSLorentzendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSLorentzopen CKSMixedGeometrylocal instance real_isTopologicalAddGroup : IsTopologicalAddGroup ℝ := inferInstancelocal instance spatialDual_isTopologicalAddGroup : IsTopologicalAddGroup (OAI.CKSLorentz.E →L[ℝ] ℝ) := inferInstancelocal instance spatialDual_smulCommClass : letI := OAI.CKSLorentz.real_smulCommClass SMulCommClass ℝ ℝ (OAI.CKSLorentz.E →L[ℝ] ℝ) := inferInstancelocal instance spatialDual_continuousConstSMul : ContinuousConstSMul ℝ (OAI.CKSLorentz.E →L[ℝ] ℝ) := inferInstancelocal instance spatialDual_isScalarTower : IsScalarTower ℝ ℝ (OAI.CKSLorentz.E →L[ℝ] ℝ) := inferInstancelocal instance spatialDual_continuousSMul : ContinuousSMul ℝ (OAI.CKSLorentz.E →L[ℝ] ℝ) := inferInstancedef hyperbolicField (x : OAI.CKSLorentz.E) : OAI.CKSLorentz.SpatialBilinear := letI := OAI.CKSLorentz.real_continuousAdd letI := OAI.CKSLorentz.real_continuousConstSMul letI := OAI.CKSLorentz.real_smulCommClass letI := OAI.CKSLorentz.real_isTopologicalAddGroup letI := OAI.CKSLorentz.spatialDual_isTopologicalAddGroup letI := OAI.CKSLorentz.spatialDual_smulCommClass letI := OAI.CKSLorentz.spatialDual_continuousConstSMul letI := OAI.CKSLorentz.spatialDual_isScalarTower letI := OAI.CKSLorentz.spatialDual_continuousSMul let f : OAI.CKSLorentz.SpatialBilinear := innerSL ℝ f - (1/(1+‖x‖^2)) • (f x).smulRight (f x)def sourceSpatial (A : OAI.CKSLorentz.SpatialTensor) : OAI.CKSLorentz.SpatialTensor := fun x => OAI.CKSLorentz.hyperbolicField x + A xend OAI.CKSLorentzendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSLorentzopen scoped ContDiffattribute [local instance] CKSSpatialManifold.real_id_isometric real_smulCommClass spatialDual_smulCommClasslocal instance hsgNorm : NormedAddCommGroup OAI.CKSLorentz.SpatialBilinear := let dualSpace : NormedSpace ℝ (OAI.CKSLorentz.E →L[ℝ] ℝ) := @ContinuousLinearMap.toNormedSpace ℝ ℝ OAI.CKSLorentz.E ℝ _ _ _ _ _ _ (RingHom.id ℝ) OAI.CKSSpatialManifold.real_id_isometric ℝ _ _ OAI.CKSLorentz.real_smulCommClass @ContinuousLinearMap.toNormedAddCommGroup ℝ ℝ OAI.CKSLorentz.E (OAI.CKSLorentz.E →L[ℝ] ℝ) _ _ _ _ _ dualSpace (RingHom.id ℝ) OAI.CKSSpatialManifold.real_id_isometricend OAI.CKSLorentzendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSLorentzopen scoped ContDiffattribute [local instance] CKSSpatialManifold.real_id_isometric real_smulCommClass spatialDual_smulCommClassattribute [local instance] OAI.CKSLorentz.hsgNormlocal instance hsgSpace : NormedSpace ℝ OAI.CKSLorentz.SpatialBilinear := let dualSpace : NormedSpace ℝ (OAI.CKSLorentz.E →L[ℝ] ℝ) := @ContinuousLinearMap.toNormedSpace ℝ ℝ OAI.CKSLorentz.E ℝ _ _ _ _ _ _ (RingHom.id ℝ) OAI.CKSSpatialManifold.real_id_isometric ℝ _ _ OAI.CKSLorentz.real_smulCommClass @ContinuousLinearMap.toNormedSpace ℝ ℝ OAI.CKSLorentz.E (OAI.CKSLorentz.E →L[ℝ] ℝ) _ _ _ _ _ dualSpace (RingHom.id ℝ) OAI.CKSSpatialManifold.real_id_isometric ℝ _ dualSpace OAI.CKSLorentz.spatialDual_smulCommClassend OAI.CKSLorentzendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSADMopen Finset CKSInducedSphereopen scoped RealInnerProductSpace ContDiffdef normal (x : OAI.CKSInducedSphere.E) (i : OAI.CKSInducedSphere.Ix) : ℝ := x i / ‖x‖end OAI.CKSADMendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSADMopen Set Filter Finset CKSSphericalHarmonics CKSInducedSphereopen scoped Topology ContDiffdef spatialInfinity : Filter OAI.CKSInducedSphere.E := Filter.comap (fun x : OAI.CKSInducedSphere.E => ‖x‖) atTopdef TailRegular (F : OAI.CKSInducedSphere.E → ℝ) : Prop := ∀ᶠ x in OAI.CKSADM.spatialInfinity, ContDiffAt ℝ ∞ F xdef Decay (d : ℝ) (F : OAI.CKSInducedSphere.E → ℝ) : Prop := ∃ C : ℝ, 0 ≤ C ∧ ∀ᶠ x in OAI.CKSADM.spatialInfinity, |F x| ≤ C*‖x‖^(-d)def SymbolN : ℕ → ℝ → (OAI.CKSInducedSphere.E → ℝ) → Prop | 0, d, F => OAI.CKSADM.Decay d F | n+1, d, F => OAI.CKSADM.Decay d F ∧ ∀ j : OAI.CKSInducedSphere.Ix, SymbolN n (d+1) (OAI.CKSInducedSphere.pd j F)def Symbol (d : ℝ) (F : OAI.CKSInducedSphere.E → ℝ) : Prop := OAI.CKSADM.TailRegular F ∧ ∀ n : ℕ, OAI.CKSADM.SymbolN n d Fend OAI.CKSADMendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSAngularGeometryopen Matrix CKSCalculus Filteropen scoped BigOperators Topology ContDiff Matrix.Norms.Elementwisedef physicalMetricJet (G : OAI.CKSAngularGeometry.PhysicalPoint → OAI.CKSAngularGeometry.AmbientMat) (x : OAI.CKSAngularGeometry.PhysicalPoint) : OAI.CKSRound.MetricJet where inv := (G x)⁻¹ d := fun a i j => OAI.CKSCalculus.D (OAI.CKSRealizedRound.basis a) (fun y => G y i j) x dd := fun a b i j => OAI.CKSCalculus.D (OAI.CKSRealizedRound.basis a) (OAI.CKSCalculus.D (OAI.CKSRealizedRound.basis b) (fun y => G y i j)) xdef physicalTensorJet (K : OAI.CKSAngularGeometry.PhysicalPoint → OAI.CKSAngularGeometry.AmbientMat) (x : OAI.CKSAngularGeometry.PhysicalPoint) : OAI.CKSRound.TensorJet where val := K x d := fun a i j => OAI.CKSCalculus.D (OAI.CKSRealizedRound.basis a) (fun y => K y i j) xend OAI.CKSAngularGeometryendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSCartesianOuteropen Set Filter Matrix CKSADM CKSInducedSphere CKSSphericalHarmonicsopen CKSAngularGeometry (PhysicalPoint)open scoped Topology ContDiff Matrix.Norms.Elementwiseabbrev toPoint : OAI.CKSInducedSphere.E ≃L[ℝ] OAI.CKSAngularGeometry.PhysicalPoint := EuclideanSpace.equiv (Fin 3) ℝend OAI.CKSCartesianOuterendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSLorentzopen CKSMixedGeometry CKSAngularSlice CKSCalculusdef cksChartMassAspect (φ : OAI.CKSMixedGeometry.Angle → OAI.CKSLorentz.E) (mr : OAI.CKSMixedGeometry.Angle → ℝ) (mg mK : OAI.CKSMixedGeometry.I → OAI.CKSMixedGeometry.I → OAI.CKSMixedGeometry.Angle → ℝ) (θ : OAI.CKSMixedGeometry.Angle) : ℝ := letI := OAI.CKSLorentz.two_atLeastTwo OAI.CKSLorentz.angularMetricTrace (OAI.CKSLorentz.angularRoundMetric φ θ) (fun a b => mg a.succ b.succ θ + 2*mK a.succ b.succ θ) + 2*mr θend OAI.CKSLorentzendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSLorentzopen CKSMixedGeometry CKSAngularGeometrydef spatialCoefficients (A : OAI.CKSLorentz.SpatialTensor) (y : OAI.CKSAngularGeometry.PhysicalPoint) : OAI.CKSAngularGeometry.AmbientMat := fun i j => A (OAI.CKSCartesianOuter.toPoint.symm y) (OAI.CKSCartesianOuter.toPoint.symm (OAI.CKSMixedGeometry.basis i)) (OAI.CKSCartesianOuter.toPoint.symm (OAI.CKSMixedGeometry.basis j))def spatialDEC (A B : OAI.CKSLorentz.SpatialTensor) (x : OAI.CKSLorentz.E) : Prop := OAI.CKSLocalBending.DEC (OAI.CKSAngularGeometry.physicalMetricJet (OAI.CKSLorentz.spatialCoefficients A) (OAI.CKSCartesianOuter.toPoint x)) (OAI.CKSAngularGeometry.physicalTensorJet (OAI.CKSLorentz.spatialCoefficients B) (OAI.CKSCartesianOuter.toPoint x))end OAI.CKSLorentzendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSLorentzopen CKSMixedGeometry CKSAngularSlice Setdef CKSTensorPatch.RepresentsMassAspect (Q : OAI.CKSLorentz.CKSTensorPatch) (M : OAI.CKSLorentz.Sphere → ℝ) : Prop := ∀ n ∈ Q.patch.sphereRegion Q.region, OAI.CKSLorentz.cksChartMassAspect Q.patch.param Q.mr Q.mg Q.mK (Q.patch.chart n) = M nend OAI.CKSLorentzendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSLorentzopen CKSMixedGeometry CKSAngularGeometry CKSInducedSphere CKSSphericalHarmonics MeasureTheorydef spatialCartesian (A : OAI.CKSLorentz.SpatialTensor) (x : OAI.CKSLorentz.E) : OAI.CKSAngularGeometry.AmbientMat := OAI.CKSLorentz.spatialCoefficients A (OAI.CKSCartesianOuter.toPoint x)local instance sixteen_atLeastTwo : Nat.AtLeastTwo 16 := inferInstanceend OAI.CKSLorentzendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSLorentzopen CKSMixedGeometry CKSAngularGeometry CKSInducedSphere CKSSphericalHarmonics MeasureTheoryattribute [local instance] sixteen_atLeastTwodef spatialADMEnergy (A : OAI.CKSLorentz.SpatialTensor) (r : ℝ) : ℝ := r^2/(16*Real.pi) * ∫ n : OAI.CKSLorentz.Sphere, ∑ i : Fin 3, (∑ j : Fin 3, (OAI.CKSInducedSphere.pd j (fun y => OAI.CKSLorentz.spatialCartesian A y i j) (r • (n:OAI.CKSLorentz.E)) - OAI.CKSInducedSphere.pd i (fun y => OAI.CKSLorentz.spatialCartesian A y j j) (r • (n:OAI.CKSLorentz.E)))) * OAI.CKSADM.normal (r • (n:OAI.CKSLorentz.E)) i ∂OAI.CKSSphericalHarmonics.surfaceMeasuredef spatialADMMomentum (A B : OAI.CKSLorentz.SpatialTensor) (r : ℝ) : Fin 3 → ℝ := fun i => r^2/(8*Real.pi) * ∫ n : OAI.CKSLorentz.Sphere, ∑ j : Fin 3, (OAI.CKSLorentz.spatialCartesian B (r • (n:OAI.CKSLorentz.E)) i j - (∑ a : Fin 3, ∑ b : Fin 3, (OAI.CKSLorentz.spatialCartesian A (r • (n:OAI.CKSLorentz.E)))⁻¹ a b * OAI.CKSLorentz.spatialCartesian B (r • (n:OAI.CKSLorentz.E)) a b) * OAI.CKSLorentz.spatialCartesian A (r • (n:OAI.CKSLorentz.E)) i j) * OAI.CKSADM.normal (r • (n:OAI.CKSLorentz.E)) j ∂OAI.CKSSphericalHarmonics.surfaceMeasureend OAI.CKSLorentzendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSLorentzopen CKSMixedGeometry CKSAngularGeometry MeasureTheorydef spatialEnergy (A B : OAI.CKSLorentz.SpatialTensor) (x : OAI.CKSLorentz.E) : ℝ := (OAI.CKSAngularGeometry.physicalMetricJet (OAI.CKSLorentz.spatialCoefficients A) (OAI.CKSCartesianOuter.toPoint x)).energy (OAI.CKSAngularGeometry.physicalTensorJet (OAI.CKSLorentz.spatialCoefficients B) (OAI.CKSCartesianOuter.toPoint x))end OAI.CKSLorentzendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSReplacementCompletenessopen Bundle Manifoldopen scoped Bundle Manifold ENNRealvariable {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M]abbrev Metric := ContinuousRiemannianMetric E (fun x : M => TangentSpace I x)local instance metric_isContinuousRiemannianBundle (g : OAI.CKSReplacementCompleteness.Metric I (M := M)) : letI : RiemannianBundle (fun x : M => TangentSpace I x) := ⟨g.toRiemannianMetric⟩ IsContinuousRiemannianBundle E (fun x : M => TangentSpace I x) := inferInstance@[instance_reducible] def metricSpace [T3Space M] (g : OAI.CKSReplacementCompleteness.Metric I (M := M)) : EMetricSpace M := letI : RiemannianBundle (fun x : M => TangentSpace I x) := ⟨g.toRiemannianMetric⟩ letI := OAI.CKSReplacementCompleteness.metric_isContinuousRiemannianBundle I g EMetricSpace.ofRiemannianMetric I Mdef IsComplete [T3Space M] (g : OAI.CKSReplacementCompleteness.Metric I (M := M)) : Prop := @CompleteSpace M (OAI.CKSReplacementCompleteness.metricSpace I g).toUniformSpaceend OAI.CKSReplacementCompletenessendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSGeometricCutsopen Set Manifold MeasureTheory Bundle CKSReplacementCompletenessopen scoped ENNReal Manifold Bundle ContDiffabbrev E3 := EuclideanSpace ℝ (Fin 3)local instance halfSpaceDimension_neZero : NeZero (3 : ℕ) := inferInstanceabbrev H3 := @EuclideanHalfSpace 3 OAI.CKSGeometricCuts.halfSpaceDimension_neZeroabbrev I3 := @modelWithCornersEuclideanHalfSpace 3 OAI.CKSGeometricCuts.halfSpaceDimension_neZeroend OAI.CKSGeometricCutsendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSGeometricCutsopen Set Manifold MeasureTheory Bundle CKSReplacementCompletenessopen scoped ENNReal Manifold Bundle ContDiffvariable (M : Type u) [TopologicalSpace M] [ChartedSpace H3 M] [IsManifold I3 1 M]structure OuterDomain where Carrier : Type u topology : TopologicalSpace Carrier charts : @ChartedSpace OAI.CKSGeometricCuts.H3 _ Carrier topology smooth : @IsManifold ℝ _ OAI.CKSGeometricCuts.E3 _ _ OAI.CKSGeometricCuts.H3 _ OAI.CKSGeometricCuts.I3 (∞ : ℕ∞ω) Carrier topology charts inclusion : Carrier → M embedding : @IsSmoothEmbedding ℝ _ OAI.CKSGeometricCuts.E3 OAI.CKSGeometricCuts.E3 _ _ _ _ OAI.CKSGeometricCuts.H3 OAI.CKSGeometricCuts.H3 _ _ OAI.CKSGeometricCuts.I3 OAI.CKSGeometricCuts.I3 Carrier M topology charts _ _ ∞ inclusion closed : IsClosed (range inclusion) connected : IsConnected (range inclusion) contains_distant_end : ∃ K : Set M, IsCompact K ∧ Kᶜ ⊆ range inclusion interior_into : inclusion '' (@ModelWithCorners.interior ℝ _ OAI.CKSGeometricCuts.E3 _ _ OAI.CKSGeometricCuts.H3 _ OAI.CKSGeometricCuts.I3 Carrier topology charts) ⊆ OAI.CKSGeometricCuts.I3.interior M compact_boundary : IsCompact (inclusion '' (@ModelWithCorners.boundary ℝ _ OAI.CKSGeometricCuts.E3 _ _ OAI.CKSGeometricCuts.H3 _ OAI.CKSGeometricCuts.I3 Carrier topology charts))end OAI.CKSGeometricCutsendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSSpatialManifoldopen Bundle Manifold Set Bornology Filter CKSLorentz CKSMetricGluingopen scoped Bundle Manifold ContDiff Topologyvariable {H : Type*} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type*} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I ∞ M]attribute [local instance] real_id_isometric CKSMetricGluing.real_continuousAdd CKSMetricGluing.real_continuousConstSMul CKSMetricGluing.real_smulCommClasslocal instance real_id_compTriple : RingHomCompTriple (RingHom.id ℝ) (RingHom.id ℝ) (RingHom.id ℝ) := inferInstanceend OAI.CKSSpatialManifoldendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSSpatialManifoldopen Bundle Manifold Set Bornology Filter CKSLorentz CKSMetricGluingopen scoped Bundle Manifold ContDiff Topologyvariable {H : Type u_1} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_2} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I ∞ M]attribute [local instance] real_id_isometric CKSMetricGluing.real_continuousAdd CKSMetricGluing.real_continuousConstSMul CKSMetricGluing.real_smulCommClassdef endInner (f : M → OAI.CKSLorentz.E) (A : OAI.CKSLorentz.SpatialTensor) : OAI.CKSMetricGluing.InnerField I (M := M) := fun x => by letI := OAI.CKSSpatialManifold.real_id_isometric letI := OAI.CKSSpatialManifold.real_id_compTriple letI : NormedAddCommGroup (TangentSpace I x) := by unfold TangentSpace; infer_instance letI : NormedSpace ℝ (TangentSpace I x) := by unfold TangentSpace; infer_instance let df : TangentSpace I x →L[ℝ] OAI.CKSLorentz.E := (NormedSpace.fromTangentSpace (f x)).toContinuousLinearMap.comp (mfderiv I 𝓘(ℝ,OAI.CKSLorentz.E) f x) exact (A (f x)).bilinearComp df dfend OAI.CKSSpatialManifoldendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSSpatialManifoldopen Bundle Manifold Set Filter CKSLorentz CKSMetricGluingopen scoped Bundle Manifold ContDiff Topologyvariable {H : Type u_1} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_2} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I ∞ M]attribute [local instance] CKSLorentz.hsgNorm CKSLorentz.hsgSpacedef PhysicalDECAt (g : OAI.CKSMetricGluing.InnerField I (M := M)) (K : OAI.CKSMetricGluing.InnerField I (M := M)) (x : M) : Prop := ∃ (V : Set M) (f : M → OAI.CKSLorentz.E) (A B : OAI.CKSLorentz.SpatialTensor), IsOpen V ∧ x ∈ V ∧ ContMDiffOn I 𝓘(ℝ,OAI.CKSLorentz.E) ∞ f V ∧ (∀ y ∈ V, Function.Bijective (mfderiv I 𝓘(ℝ,OAI.CKSLorentz.E) f y)) ∧ (∀ y ∈ V, ContDiffAt ℝ ∞ A (f y) ∧ ContDiffAt ℝ ∞ B (f y)) ∧ (∀ y ∈ V, (∀ v w, A (f y) v w = A (f y) w v) ∧ (∀ v : OAI.CKSLorentz.E, v ≠ 0 → 0 < A (f y) v v) ∧ (∀ v w, B (f y) v w = B (f y) w v)) ∧ (∀ y ∈ V, g y = OAI.CKSSpatialManifold.endInner I f A y ∧ K y = OAI.CKSSpatialManifold.endInner I f B y) ∧ OAI.CKSLorentz.spatialDEC A B (f x)def PhysicalDEC (g : OAI.CKSMetricGluing.InnerField I (M := M)) (K : OAI.CKSMetricGluing.InnerField I (M := M)) : Prop := ∀ x : M, OAI.CKSSpatialManifold.PhysicalDECAt I g K xend OAI.CKSSpatialManifoldendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSIntrinsicGeometryopen Bundle Bornology Set MeasureTheory Manifold Filter Metricopen scoped ENNReal ContDiff Topology NNReallocal instance halfSpaceDimension_neZero : NeZero (3 : ℕ) := inferInstanceabbrev H3 := @EuclideanHalfSpace 3 OAI.CKSIntrinsicGeometry.halfSpaceDimension_neZeroabbrev I3 := @modelWithCornersEuclideanHalfSpace 3 OAI.CKSIntrinsicGeometry.halfSpaceDimension_neZeroend OAI.CKSIntrinsicGeometryendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSBoundarySurfaceopen Set Manifold Bundle Filteropen scoped ContDiff Topologyabbrev E2 := EuclideanSpace ℝ (Fin 2)abbrev E3 := EuclideanSpace ℝ (Fin 3)local instance halfSpaceDimension_neZero : NeZero (3 : ℕ) := inferInstanceabbrev H3 := @EuclideanHalfSpace 3 OAI.CKSBoundarySurface.halfSpaceDimension_neZeroabbrev I2 := 𝓘(ℝ,OAI.CKSBoundarySurface.E2)abbrev I3 := @modelWithCornersEuclideanHalfSpace 3 OAI.CKSBoundarySurface.halfSpaceDimension_neZerolocal instance two_atLeastTwo : Nat.AtLeastTwo 2 := inferInstanceend OAI.CKSBoundarySurfaceendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSBoundarySurfaceopen Set Manifold Bundle Filteropen scoped ContDiff Topologyattribute [local instance] two_atLeastTwodef insertNormalZero (point : OAI.CKSBoundarySurface.E2) : OAI.CKSBoundarySurface.E3 := WithLp.toLp 2 (Fin.cons 0 point)def liftPlane : OAI.CKSBoundarySurface.E2 →L[ℝ] OAI.CKSBoundarySurface.E3 := have proof_insertNormalZero_add_0 (first second : OAI.CKSBoundarySurface.E2) : OAI.CKSBoundarySurface.insertNormalZero (first + second) = OAI.CKSBoundarySurface.insertNormalZero first + OAI.CKSBoundarySurface.insertNormalZero second := by ext index cases index using Fin.cases <;> simp [OAI.CKSBoundarySurface.insertNormalZero] have proof_insertNormalZero_smul_1 (scalar : ℝ) (point : OAI.CKSBoundarySurface.E2) : OAI.CKSBoundarySurface.insertNormalZero (scalar • point) = scalar • OAI.CKSBoundarySurface.insertNormalZero point := by ext index cases index using Fin.cases <;> simp [OAI.CKSBoundarySurface.insertNormalZero] have proof_insertNormalZero_continuous_2 : Continuous OAI.CKSBoundarySurface.insertNormalZero := by apply (PiLp.continuous_toLp 2 (fun _ : Fin 3 => ℝ)).comp apply continuous_pi intro index cases index using Fin.cases with | zero => exact continuous_const | succ index => exact PiLp.continuous_apply 2 (fun _ : Fin 2 => ℝ) index { toFun := OAI.CKSBoundarySurface.insertNormalZero map_add' := proof_insertNormalZero_add_0 map_smul' := proof_insertNormalZero_smul_1 cont := proof_insertNormalZero_continuous_2 }def tangentialCoordinates (point : OAI.CKSBoundarySurface.E3) : OAI.CKSBoundarySurface.E2 := WithLp.toLp 2 (fun index => point index.succ)def dropPlane : OAI.CKSBoundarySurface.E3 →L[ℝ] OAI.CKSBoundarySurface.E2 := have proof_tangentialCoordinates_add_3 (first second : OAI.CKSBoundarySurface.E3) : OAI.CKSBoundarySurface.tangentialCoordinates (first + second) = OAI.CKSBoundarySurface.tangentialCoordinates first + OAI.CKSBoundarySurface.tangentialCoordinates second := by ext index simp [OAI.CKSBoundarySurface.tangentialCoordinates] have proof_tangentialCoordinates_smul_4 (scalar : ℝ) (point : OAI.CKSBoundarySurface.E3) : OAI.CKSBoundarySurface.tangentialCoordinates (scalar • point) = scalar • OAI.CKSBoundarySurface.tangentialCoordinates point := by ext index simp [OAI.CKSBoundarySurface.tangentialCoordinates] have proof_tangentialCoordinates_continuous_5 : Continuous OAI.CKSBoundarySurface.tangentialCoordinates := by apply (PiLp.continuous_toLp 2 (fun _ : Fin 2 => ℝ)).comp exact continuous_pi fun index => PiLp.continuous_apply 2 (fun _ : Fin 3 => ℝ) index.succ { toFun := OAI.CKSBoundarySurface.tangentialCoordinates map_add' := proof_tangentialCoordinates_add_3 map_smul' := proof_tangentialCoordinates_smul_4 cont := proof_tangentialCoordinates_continuous_5 }end OAI.CKSBoundarySurfaceendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSBoundarySurfaceopen Set Manifold Bundle Filteropen scoped ContDiff Topologydef liftHalf (z : OAI.CKSBoundarySurface.E2) : OAI.CKSBoundarySurface.H3 := have proof_liftPlane_zero_6 (z : OAI.CKSBoundarySurface.E2) : OAI.CKSBoundarySurface.liftPlane z 0 = 0 := rfl have proof_liftPlane_succ_7 (z : OAI.CKSBoundarySurface.E2) (i : Fin 2) : OAI.CKSBoundarySurface.liftPlane z i.succ = z i := rfl ⟨OAI.CKSBoundarySurface.liftPlane z, by simp [*]⟩end OAI.CKSBoundarySurfaceendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSSchwarzschildopen Set Manifold Bundle Filteropen scoped ContDiff Topologyopen CKSBoundarySurfaceabbrev Radial := {t : ℝ // 0 ≤ t}abbrev Sphere := Metric.sphere (0 : OAI.CKSBoundarySurface.E3) 1abbrev Exterior := OAI.CKSSchwarzschild.Radial × OAI.CKSSchwarzschild.Sphereend OAI.CKSSchwarzschildendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSSchwarzschildopen Set Manifold Bundle Filteropen scoped ContDiff Topologyopen CKSBoundarySurfaceattribute [local instance] Classical.propDecidablelocal instance real_id_invPair : RingHomInvPair (RingHom.id ℝ) (RingHom.id ℝ) := inferInstancedef join : (ℝ × OAI.CKSBoundarySurface.E2) →L[ℝ] OAI.CKSBoundarySurface.E3 := letI := OAI.CKSSchwarzschild.real_id_invPair letI := OAI.CKSBoundarySurface.two_atLeastTwo let continuousLinearMap : ((ℝ × OAI.CKSBoundarySurface.E2) →ₗ[ℝ] OAI.CKSBoundarySurface.E3) ≃ₗ[ℝ] ((ℝ × OAI.CKSBoundarySurface.E2) →L[ℝ] OAI.CKSBoundarySurface.E3) := LinearMap.toContinuousLinearMap continuousLinearMap { toFun := fun z => WithLp.toLp 2 (Fin.cons z.1 z.2) map_add' := by intro a b; ext i; cases i using Fin.cases <;> simp map_smul' := by intro a b; ext i; cases i using Fin.cases <;> simp }def halfProduct : OAI.CKSSchwarzschild.Radial × OAI.CKSBoundarySurface.E2 ≃ₜ OAI.CKSBoundarySurface.H3 := have proof_join_zero_9 (z : ℝ × OAI.CKSBoundarySurface.E2) : OAI.CKSSchwarzschild.join z 0 = z.1 := rfl have proof_join_succ_10 (z : ℝ × OAI.CKSBoundarySurface.E2) (i : Fin 2) : OAI.CKSSchwarzschild.join z i.succ = z.2 i := rfl have proof_join_drop_8 (z : OAI.CKSBoundarySurface.E3) : OAI.CKSSchwarzschild.join (z 0,OAI.CKSBoundarySurface.dropPlane z) = z := by ext i; cases i using Fin.cases <;> rfl have proof_drop_join_11 (z : ℝ × OAI.CKSBoundarySurface.E2) : OAI.CKSBoundarySurface.dropPlane (OAI.CKSSchwarzschild.join z) = z.2 := by ext i; rfl letI := OAI.CKSBoundarySurface.halfSpaceDimension_neZero { toFun z := ⟨OAI.CKSSchwarzschild.join (z.1.val,z.2),z.1.property⟩ invFun z := (⟨z.val 0,z.property⟩,OAI.CKSBoundarySurface.dropPlane z.val) left_inv z := by cases z; simp [*] right_inv z := by apply Subtype.ext; exact proof_join_drop_8 _ continuous_toFun := (OAI.CKSSchwarzschild.join.continuous.comp ((continuous_subtype_val.comp continuous_fst).prodMk continuous_snd)).subtype_mk _ continuous_invFun := ((by fun_prop : Continuous (fun z : H3 => z.val 0)).subtype_mk _).prodMk (OAI.CKSBoundarySurface.dropPlane.continuous.comp continuous_subtype_val) }def productChart (s : OAI.CKSSchwarzschild.Sphere) : OpenPartialHomeomorph OAI.CKSSchwarzschild.Exterior OAI.CKSBoundarySurface.H3 := ((OpenPartialHomeomorph.refl OAI.CKSSchwarzschild.Radial).prod (chartAt OAI.CKSBoundarySurface.E2 s)).trans OAI.CKSSchwarzschild.halfProduct.toOpenPartialHomeomorphinstance exteriorChartedSpace : ChartedSpace OAI.CKSBoundarySurface.H3 OAI.CKSSchwarzschild.Exterior := have proof_join_zero_9 (z : ℝ × OAI.CKSBoundarySurface.E2) : OAI.CKSSchwarzschild.join z 0 = z.1 := rfl have proof_join_succ_10 (z : ℝ × OAI.CKSBoundarySurface.E2) (i : Fin 2) : OAI.CKSSchwarzschild.join z i.succ = z.2 i := rfl have proof_halfProduct_val_12 (z : OAI.CKSSchwarzschild.Radial × OAI.CKSBoundarySurface.E2) : (OAI.CKSSchwarzschild.halfProduct z).val = OAI.CKSSchwarzschild.join (z.1.val,z.2) := rfl have proof_halfProduct_symm_fst_13 (z : OAI.CKSBoundarySurface.H3) : (OAI.CKSSchwarzschild.halfProduct.symm z).1.val = z.val 0 := rfl have proof_halfProduct_symm_snd_14 (z : OAI.CKSBoundarySurface.H3) : (OAI.CKSSchwarzschild.halfProduct.symm z).2 = OAI.CKSBoundarySurface.dropPlane z.val := rfl { atlas := range OAI.CKSSchwarzschild.productChart chartAt p := OAI.CKSSchwarzschild.productChart p.2 mem_chart_source p := by simp [*, OAI.CKSSchwarzschild.productChart,mem_chart_source OAI.CKSBoundarySurface.E2 p.2] chart_mem_atlas p := mem_range_self _ }end OAI.CKSSchwarzschildendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSSchwarzschildopen Set Manifold Bundle Filteropen scoped ContDiff Topologyopen CKSBoundarySurfaceattribute [local instance] halfSpaceDimension_neZeroinstance exteriorIsManifold : IsManifold OAI.CKSBoundarySurface.I3 ∞ OAI.CKSSchwarzschild.Exterior := have proof_join_zero_9 (z : ℝ × OAI.CKSBoundarySurface.E2) : OAI.CKSSchwarzschild.join z 0 = z.1 := rfl have proof_join_succ_10 (z : ℝ × OAI.CKSBoundarySurface.E2) (i : Fin 2) : OAI.CKSSchwarzschild.join z i.succ = z.2 i := rfl have proof_halfProduct_val_12 (z : OAI.CKSSchwarzschild.Radial × OAI.CKSBoundarySurface.E2) : (OAI.CKSSchwarzschild.halfProduct z).val = OAI.CKSSchwarzschild.join (z.1.val,z.2) := rfl have proof_halfProduct_symm_fst_13 (z : OAI.CKSBoundarySurface.H3) : (OAI.CKSSchwarzschild.halfProduct.symm z).1.val = z.val 0 := rfl have proof_halfProduct_symm_snd_14 (z : OAI.CKSBoundarySurface.H3) : (OAI.CKSSchwarzschild.halfProduct.symm z).2 = OAI.CKSBoundarySurface.dropPlane z.val := rfl have proof_productChart_target_17 (s : OAI.CKSSchwarzschild.Sphere) : (OAI.CKSSchwarzschild.productChart s).target = (fun z : OAI.CKSBoundarySurface.H3 => OAI.CKSBoundarySurface.dropPlane z.val) ⁻¹' (chartAt OAI.CKSBoundarySurface.E2 s).target := by ext p; simp [*, OAI.CKSSchwarzschild.productChart] have proof_productChart_source_18 (s : OAI.CKSSchwarzschild.Sphere) : (OAI.CKSSchwarzschild.productChart s).source = Prod.snd ⁻¹' (chartAt OAI.CKSBoundarySurface.E2 s).source := by ext p; simp [*, OAI.CKSSchwarzschild.productChart] have proof_productChart_symm_19 (s : OAI.CKSSchwarzschild.Sphere) (z : OAI.CKSBoundarySurface.H3) : (OAI.CKSSchwarzschild.productChart s).symm z = (⟨z.val 0,z.property⟩,(chartAt OAI.CKSBoundarySurface.E2 s).symm (OAI.CKSBoundarySurface.dropPlane z.val)) := rfl have proof_transition_source_20 (a b : OAI.CKSSchwarzschild.Sphere) : ((OAI.CKSSchwarzschild.productChart a).symm ≫ₕ OAI.CKSSchwarzschild.productChart b).source = (fun z : OAI.CKSBoundarySurface.H3 => OAI.CKSBoundarySurface.dropPlane z.val) ⁻¹' ((chartAt OAI.CKSBoundarySurface.E2 a).symm ≫ₕ chartAt OAI.CKSBoundarySurface.E2 b).source := by ext z simp only [OpenPartialHomeomorph.trans_source,OpenPartialHomeomorph.symm_source, mem_inter_iff,mem_preimage,proof_productChart_target_17,proof_productChart_source_18,proof_productChart_symm_19] have proof_transition_maps_15 (a b : OAI.CKSSchwarzschild.Sphere) : MapsTo OAI.CKSBoundarySurface.dropPlane (OAI.CKSBoundarySurface.I3.symm ⁻¹' ((OAI.CKSSchwarzschild.productChart a).symm ≫ₕ OAI.CKSSchwarzschild.productChart b).source ∩ range OAI.CKSBoundarySurface.I3) ((extChartAt OAI.CKSBoundarySurface.I2 a).symm ≫ extChartAt OAI.CKSBoundarySurface.I2 b).source := by intro z hz have he : (OAI.CKSBoundarySurface.I3.symm z).val = z := OAI.CKSBoundarySurface.I3.right_inv hz.2 have h := hz.1 rw [proof_transition_source_20] at h change OAI.CKSBoundarySurface.dropPlane (OAI.CKSBoundarySurface.I3.symm z).val ∈ ((chartAt OAI.CKSBoundarySurface.E2 a).symm ≫ₕ chartAt OAI.CKSBoundarySurface.E2 b).source at h rw [he] at h simpa only [OAI.CKSBoundarySurface.I2,extChartAt_model_space_eq_id,mfld_simps] using h have proof_transition_formula_16 (a b : OAI.CKSSchwarzschild.Sphere) {z : OAI.CKSBoundarySurface.E3} (hz : z ∈ range OAI.CKSBoundarySurface.I3) : OAI.CKSBoundarySurface.I3 (((OAI.CKSSchwarzschild.productChart a).symm ≫ₕ OAI.CKSSchwarzschild.productChart b) (OAI.CKSBoundarySurface.I3.symm z)) = OAI.CKSSchwarzschild.join (z 0,((extChartAt OAI.CKSBoundarySurface.I2 a).symm ≫ extChartAt OAI.CKSBoundarySurface.I2 b) (OAI.CKSBoundarySurface.dropPlane z)) := by have he : (OAI.CKSBoundarySurface.I3.symm z).val = z := OAI.CKSBoundarySurface.I3.right_inv hz change OAI.CKSSchwarzschild.join ((OAI.CKSBoundarySurface.I3.symm z).val 0, chartAt OAI.CKSBoundarySurface.E2 b ((chartAt OAI.CKSBoundarySurface.E2 a).symm (OAI.CKSBoundarySurface.dropPlane (OAI.CKSBoundarySurface.I3.symm z).val))) = _ rw [he] rfl by apply isManifold_of_contDiffOn rintro e e' ⟨a,rfl⟩ ⟨b,rfl⟩ change ContDiffOn ℝ ∞ (fun z => OAI.CKSBoundarySurface.I3 (((OAI.CKSSchwarzschild.productChart a).symm ≫ₕ OAI.CKSSchwarzschild.productChart b) (OAI.CKSBoundarySurface.I3.symm z))) (OAI.CKSBoundarySurface.I3.symm ⁻¹' ((OAI.CKSSchwarzschild.productChart a).symm ≫ₕ OAI.CKSSchwarzschild.productChart b).source ∩ range OAI.CKSBoundarySurface.I3) have hs := (contDiffOn_ext_coord_change (I := OAI.CKSBoundarySurface.I2) (n := ∞) b a).comp OAI.CKSBoundarySurface.dropPlane.contDiff.contDiffOn (proof_transition_maps_15 a b) have h0 : ContDiff ℝ ∞ (fun z : OAI.CKSBoundarySurface.E3 => z 0) := by fun_prop apply (OAI.CKSSchwarzschild.join.contDiff.comp_contDiffOn (h0.contDiffOn.prodMk hs)).congr intro z hz exact proof_transition_formula_16 a b hz.2end OAI.CKSSchwarzschildendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSSchwarzschildopen Set Filter Manifold Bundleopen scoped ContDiff Topologyopen CKSBoundarySurfacedef height (p : OAI.CKSSchwarzschild.Exterior) : ℝ := p.1.valend OAI.CKSSchwarzschildendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSSchwarzschildopen Set Filter Manifold Bundle Functionopen scoped ContDiff Topology InnerProductSpaceopen CKSBoundarySurfacedef radius (m : ℝ) (p : OAI.CKSSchwarzschild.Exterior) : ℝ := letI := OAI.CKSLorentz.two_atLeastTwo 2*m+OAI.CKSSchwarzschild.height pdef directionAmbient (p : OAI.CKSSchwarzschild.Exterior) : OAI.CKSBoundarySurface.E3 := p.2.valdef position (m : ℝ) (p : OAI.CKSSchwarzschild.Exterior) : OAI.CKSBoundarySurface.E3 := OAI.CKSSchwarzschild.radius m p • OAI.CKSSchwarzschild.directionAmbient pend OAI.CKSSchwarzschildendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSSchwarzschildopen Set Filteropen scoped ContDiff Topologydef velocity (m r : ℝ) : ℝ := letI := OAI.CKSLorentz.two_atLeastTwo; -1 + (r+1)*Real.smoothTransition (r-2*m-1)def lapseSquared (m r : ℝ) : ℝ := letI := OAI.CKSLorentz.two_atLeastTwo 1-2*m/r+(OAI.CKSSchwarzschild.velocity m r)^2def lapse (m r : ℝ) : ℝ := Real.sqrt (OAI.CKSSchwarzschild.lapseSquared m r)end OAI.CKSSchwarzschildendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSSchwarzschildopen Manifold Bundle Set Filter CKSLorentz CKSMetricGluing CKSSpatialManifoldopen scoped ContDiff Topology InnerProductSpaceopen CKSBoundarySurfacedef euclideanForm : OAI.CKSLorentz.SpatialBilinear := innerSL ℝdef radialUnit (x : OAI.CKSBoundarySurface.E3) : OAI.CKSBoundarySurface.E3 := ‖x‖⁻¹ • xlocal instance real_isScalarTower : IsScalarTower ℝ ℝ ℝ := inferInstancedef radialForm (x : OAI.CKSBoundarySurface.E3) : OAI.CKSLorentz.SpatialBilinear := letI := OAI.CKSSpatialManifold.real_id_compTriple letI := OAI.CKSSpatialManifold.real_id_isometric letI := OAI.CKSSchwarzschild.real_isScalarTower letI := OAI.CKSLorentz.real_smulCommClass letI := OAI.CKSLorentz.real_isTopologicalAddGroup letI := OAI.CKSLorentz.real_continuousAdd letI := OAI.CKSLorentz.real_continuousConstSMul let innerForm : OAI.CKSLorentz.SpatialBilinear := innerSL ℝ (ContinuousLinearMap.mul ℝ ℝ).bilinearComp (innerForm (OAI.CKSSchwarzschild.radialUnit x)) (innerForm (OAI.CKSSchwarzschild.radialUnit x))local instance spatialDual_continuousAdd : ContinuousAdd (OAI.CKSBoundarySurface.E3 →L[ℝ] ℝ) := inferInstancedef cartMetric (m : ℝ) (x : OAI.CKSBoundarySurface.E3) : OAI.CKSLorentz.SpatialBilinear := letI := OAI.CKSLorentz.real_continuousAdd letI := OAI.CKSLorentz.real_continuousConstSMul letI := OAI.CKSLorentz.real_smulCommClass letI := OAI.CKSSchwarzschild.spatialDual_continuousAdd letI := OAI.CKSLorentz.spatialDual_smulCommClass letI := OAI.CKSLorentz.spatialDual_continuousConstSMul OAI.CKSSchwarzschild.euclideanForm + ((OAI.CKSSchwarzschild.lapseSquared m ‖x‖)⁻¹-1) • OAI.CKSSchwarzschild.radialForm xdef cartTensor (m : ℝ) (x : OAI.CKSBoundarySurface.E3) : OAI.CKSLorentz.SpatialBilinear := letI := OAI.CKSLorentz.real_continuousAdd letI := OAI.CKSLorentz.real_continuousConstSMul letI := OAI.CKSLorentz.real_smulCommClass letI := OAI.CKSSchwarzschild.spatialDual_continuousAdd letI := OAI.CKSLorentz.spatialDual_smulCommClass letI := OAI.CKSLorentz.spatialDual_continuousConstSMul (OAI.CKSSchwarzschild.velocity m ‖x‖ / ‖x‖) • OAI.CKSSchwarzschild.euclideanForm + (deriv (OAI.CKSSchwarzschild.velocity m) ‖x‖ / OAI.CKSSchwarzschild.lapseSquared m ‖x‖ - OAI.CKSSchwarzschild.velocity m ‖x‖ / ‖x‖) • OAI.CKSSchwarzschild.radialForm xdef metricInner (m : ℝ) : OAI.CKSMetricGluing.InnerField OAI.CKSBoundarySurface.I3 (M := OAI.CKSSchwarzschild.Exterior) := OAI.CKSSpatialManifold.endInner OAI.CKSBoundarySurface.I3 (OAI.CKSSchwarzschild.position m) (OAI.CKSSchwarzschild.cartMetric m)def tensorInner (m : ℝ) : OAI.CKSMetricGluing.InnerField OAI.CKSBoundarySurface.I3 (M := OAI.CKSSchwarzschild.Exterior) := OAI.CKSSpatialManifold.endInner OAI.CKSBoundarySurface.I3 (OAI.CKSSchwarzschild.position m) (OAI.CKSSchwarzschild.cartTensor m)end OAI.CKSSchwarzschildendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSIntrinsicConstraintsopen Bundle Manifold Set Filter CKSLorentz CKSMetricGluingopen scoped ContDiff Topologyabbrev E := OAI.CKSLorentz.Elocal instance halfSpaceDimension_neZero : NeZero (3 : ℕ) := inferInstanceabbrev H := @EuclideanHalfSpace 3 OAI.CKSIntrinsicConstraints.halfSpaceDimension_neZeroabbrev I := @modelWithCornersEuclideanHalfSpace 3 OAI.CKSIntrinsicConstraints.halfSpaceDimension_neZeroend OAI.CKSIntrinsicConstraintsendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSIntrinsicConstraintsopen Bundle Manifold Set Filter CKSLorentz CKSMetricGluingopen scoped ContDiff Topologyattribute [local instance] halfSpaceDimension_neZeroattribute [local instance] CKSSpatialManifold.real_id_isometric CKSLorentz.real_smulCommClass CKSLorentz.spatialDual_smulCommClassvariable {M : Type*} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I ∞ M]def coordinateMomentumNorm (A B : OAI.CKSLorentz.SpatialTensor) (x : OAI.CKSIntrinsicConstraints.E) : ℝ := Real.sqrt (OAI.CKSLocalBending.momentumSq (OAI.CKSAngularGeometry.physicalMetricJet (OAI.CKSLorentz.spatialCoefficients A) (OAI.CKSCartesianOuter.toPoint x)) (OAI.CKSAngularGeometry.physicalTensorJet (OAI.CKSLorentz.spatialCoefficients B) (OAI.CKSCartesianOuter.toPoint x)))end OAI.CKSIntrinsicConstraintsendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSIntrinsicConstraintsopen Bundle Manifold Set Filter CKSLorentz CKSMetricGluingopen scoped ContDiff Topologyattribute [local instance] halfSpaceDimension_neZeroattribute [local instance] CKSSpatialManifold.real_id_isometric CKSLorentz.real_smulCommClass CKSLorentz.spatialDual_smulCommClassvariable {M : Type u_1} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I ∞ M]structure ConstraintChart (g K : OAI.CKSMetricGluing.InnerField OAI.CKSIntrinsicConstraints.I (M := M)) (x : M) where domain : Set M coordinate : M → OAI.CKSIntrinsicConstraints.E metric : OAI.CKSLorentz.SpatialTensor tensor : OAI.CKSLorentz.SpatialTensor isOpen : IsOpen domain mem : x ∈ domain smooth : ContMDiffOn OAI.CKSIntrinsicConstraints.I 𝓘(ℝ,OAI.CKSIntrinsicConstraints.E) ∞ coordinate domain fullRank : ∀ y ∈ domain, Function.Bijective (mfderiv OAI.CKSIntrinsicConstraints.I 𝓘(ℝ,OAI.CKSIntrinsicConstraints.E) coordinate y) coefficientSmooth : letI := OAI.CKSLorentz.real_smulCommClass letI := OAI.CKSLorentz.spatialDual_smulCommClass ∀ y ∈ domain, ContDiffAt ℝ ∞ metric (coordinate y) ∧ ContDiffAt ℝ ∞ tensor (coordinate y) positiveSymmetric : ∀ y ∈ domain, (∀ v w, metric (coordinate y) v w = metric (coordinate y) w v) ∧ (∀ v : OAI.CKSIntrinsicConstraints.E, v ≠ 0 → 0 < metric (coordinate y) v v) ∧ (∀ v w, tensor (coordinate y) v w = tensor (coordinate y) w v) represents : ∀ y ∈ domain, g y = OAI.CKSSpatialManifold.endInner OAI.CKSIntrinsicConstraints.I coordinate metric y ∧ K y = OAI.CKSSpatialManifold.endInner OAI.CKSIntrinsicConstraints.I coordinate tensor ydef ConstraintChart.energy {g K : OAI.CKSMetricGluing.InnerField OAI.CKSIntrinsicConstraints.I (M := M)} {x : M} (c : OAI.CKSIntrinsicConstraints.ConstraintChart g K x) : ℝ := OAI.CKSLorentz.spatialEnergy c.metric c.tensor (c.coordinate x)def ConstraintChart.momentumNorm {g K : OAI.CKSMetricGluing.InnerField OAI.CKSIntrinsicConstraints.I (M := M)} {x : M} (c : OAI.CKSIntrinsicConstraints.ConstraintChart g K x) : ℝ := OAI.CKSIntrinsicConstraints.coordinateMomentumNorm c.metric c.tensor (c.coordinate x)end OAI.CKSIntrinsicConstraintsendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSIntrinsicVolumeopen Bundle Manifold Set MeasureTheoryopen scoped ContDiff ENNRealattribute [local instance] CKSIntrinsicConstraints.halfSpaceDimension_neZeroabbrev E := EuclideanSpace ℝ (Fin 3)abbrev H := @EuclideanHalfSpace 3 OAI.CKSIntrinsicConstraints.halfSpaceDimension_neZeroabbrev I := @modelWithCornersEuclideanHalfSpace 3 OAI.CKSIntrinsicConstraints.halfSpaceDimension_neZeroabbrev basis (i : Fin 3) : OAI.CKSIntrinsicVolume.E := EuclideanSpace.single i 1local instance model_finiteDimensional : FiniteDimensional ℝ OAI.CKSIntrinsicVolume.E := inferInstanceend OAI.CKSIntrinsicVolumeendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSIntrinsicVolumeopen Bundle Manifold Set MeasureTheoryopen scoped ContDiff ENNRealattribute [local instance] CKSIntrinsicConstraints.halfSpaceDimension_neZeroattribute [local instance] model_finiteDimensionallocal instance model_borelSpace : BorelSpace OAI.CKSIntrinsicVolume.E := inferInstanceend OAI.CKSIntrinsicVolumeendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSIntrinsicVolumeopen Bundle Manifold Set MeasureTheoryopen scoped ContDiff ENNRealattribute [local instance] CKSIntrinsicConstraints.halfSpaceDimension_neZerovariable {M : Type u_1} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M]abbrev Metric := ContinuousRiemannianMetric OAI.CKSIntrinsicVolume.E (fun x : M => TangentSpace OAI.CKSIntrinsicVolume.I x)def chartFrame (x : M) (y : OAI.CKSIntrinsicVolume.E) : OAI.CKSIntrinsicVolume.E →L[ℝ] TangentSpace OAI.CKSIntrinsicVolume.I ((extChartAt OAI.CKSIntrinsicVolume.I x).symm y) := mfderivWithin 𝓘(ℝ,OAI.CKSIntrinsicVolume.E) OAI.CKSIntrinsicVolume.I (extChartAt OAI.CKSIntrinsicVolume.I x).symm (range OAI.CKSIntrinsicVolume.I) ydef chartMatrix (g : OAI.CKSIntrinsicVolume.Metric (M := M)) (x : M) (y : OAI.CKSIntrinsicVolume.E) : Matrix (Fin 3) (Fin 3) ℝ := letI := OAI.CKSMetricGluing.real_continuousAdd letI := OAI.CKSMetricGluing.real_continuousConstSMul letI := OAI.CKSMetricGluing.real_smulCommClass let form : TangentSpace OAI.CKSIntrinsicVolume.I ((extChartAt OAI.CKSIntrinsicVolume.I x).symm y) →L[ℝ] TangentSpace OAI.CKSIntrinsicVolume.I ((extChartAt OAI.CKSIntrinsicVolume.I x).symm y) →L[ℝ] ℝ := g.inner ((extChartAt OAI.CKSIntrinsicVolume.I x).symm y) fun first second => form (OAI.CKSIntrinsicVolume.chartFrame x y (OAI.CKSIntrinsicVolume.basis first)) (OAI.CKSIntrinsicVolume.chartFrame x y (OAI.CKSIntrinsicVolume.basis second))def chartDensity (g : OAI.CKSIntrinsicVolume.Metric (M := M)) (x : M) (y : OAI.CKSIntrinsicVolume.E) : ℝ := Real.sqrt (OAI.CKSIntrinsicVolume.chartMatrix g x y).detend OAI.CKSIntrinsicVolumeendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSIntrinsicVolumeopen Bundle Manifold Set MeasureTheoryopen scoped ContDiff ENNRealvariable {M : Type u_1} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M]attribute [local instance] model_finiteDimensional model_borelSpacevariable [MeasurableSpace M] [BorelSpace M]def localVolume (g : OAI.CKSIntrinsicVolume.Metric (M := M)) (x : M) : Measure M := Measure.map (extChartAt OAI.CKSIntrinsicVolume.I x).symm ((volume.restrict (extChartAt OAI.CKSIntrinsicVolume.I x).target).withDensity (fun y => ENNReal.ofReal (OAI.CKSIntrinsicVolume.chartDensity g x y)))def IsVolume (g : OAI.CKSIntrinsicVolume.Metric (M := M)) (ν : Measure M) : Prop := ∀ x : M, ν.restrict (extChartAt OAI.CKSIntrinsicVolume.I x).source = OAI.CKSIntrinsicVolume.localVolume g xend OAI.CKSIntrinsicVolumeendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSIntrinsicVolumeopen Bundle Manifold Set MeasureTheoryopen scoped ContDiff ENNRealattribute [local instance] CKSIntrinsicConstraints.halfSpaceDimension_neZerovariable {M : Type u_1} [TopologicalSpace M] [ChartedSpace H M] [MeasurableSpace M] [BorelSpace M] [SecondCountableTopology M]variable [IsManifold I 1 M]def riemannianVolume (g : OAI.CKSIntrinsicVolume.Metric (M := M)) : Measure M := Classical.epsilon (fun ν => OAI.CKSIntrinsicVolume.IsVolume g ν)end OAI.CKSIntrinsicVolumeendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSBoundarySurfaceopen Set Manifold Bundle Filteropen scoped ContDiff Topologyattribute [local instance] Classical.propDecidablevariable {M : Type u_2} [TopologicalSpace M] [ChartedSpace H3 M] [@IsManifold ℝ _ E3 _ _ H3 (@instTopologicalSpaceEuclideanHalfSpace 3 halfSpaceDimension_neZero) I3 ∞ M _ _]abbrev Boundary (M : Type u_2) [TopologicalSpace M] [ChartedSpace OAI.CKSBoundarySurface.H3 M] := @ModelWithCorners.boundary ℝ _ OAI.CKSBoundarySurface.E3 _ _ OAI.CKSBoundarySurface.H3 (@instTopologicalSpaceEuclideanHalfSpace 3 OAI.CKSBoundarySurface.halfSpaceDimension_neZero) OAI.CKSBoundarySurface.I3 M _ _end OAI.CKSBoundarySurfaceendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSBoundarySurfaceopen Set Manifold Bundle Filteropen scoped ContDiff Topologyattribute [local instance] Classical.propDecidablevariable {M : Type u_1} [TopologicalSpace M] [ChartedSpace H3 M] [@IsManifold ℝ _ E3 _ _ H3 (@instTopologicalSpaceEuclideanHalfSpace 3 halfSpaceDimension_neZero) I3 ∞ M _ _]def boundaryInverse (x : OAI.CKSBoundarySurface.Boundary M) (z : OAI.CKSBoundarySurface.E2) : OAI.CKSBoundarySurface.Boundary M := have proof_boundary_chart_zero_22 {M : Type u_1} [instLocal1 : TopologicalSpace.{u_1} M] [instLocal2 : ChartedSpace.{0, u_1} OAI.CKSIntrinsicGeometry.H3 M] [instLocal3 : IsManifold.{0, 0, 0, u_1} OAI.CKSIntrinsicGeometry.I3 1 M] (x y : M) (hy : y ∈ (extChartAt OAI.CKSIntrinsicGeometry.I3 x).source) (hS : y ∈ OAI.CKSIntrinsicGeometry.I3.boundary M) : (extChartAt OAI.CKSIntrinsicGeometry.I3 x y) 0 = 0 := by have hychart : y ∈ (chartAt OAI.CKSIntrinsicGeometry.H3 x).source := by simpa using hy have hyrange : extChartAt OAI.CKSIntrinsicGeometry.I3 x y ∈ range OAI.CKSIntrinsicGeometry.I3 := (extChartAt_target_subset_range x) ((extChartAt OAI.CKSIntrinsicGeometry.I3 x).map_source hy) have hnonneg : 0 ≤ (extChartAt OAI.CKSIntrinsicGeometry.I3 x y) 0 := by simpa only [OAI.CKSIntrinsicGeometry.I3, range_modelWithCornersEuclideanHalfSpace, mem_ofPred_eq] using hyrange have hnot : ¬OAI.CKSIntrinsicGeometry.I3.IsInteriorPoint y := (OAI.CKSIntrinsicGeometry.I3.isBoundaryPoint_iff_not_isInteriorPoint y).mp hS have hle : (extChartAt OAI.CKSIntrinsicGeometry.I3 x y) 0 ≤ 0 := by by_contra h have hpos : 0 < (extChartAt OAI.CKSIntrinsicGeometry.I3 x y) 0 := lt_of_not_ge h have hint : extChartAt OAI.CKSIntrinsicGeometry.I3 x y ∈ interior (range OAI.CKSIntrinsicGeometry.I3) := by simpa only [OAI.CKSIntrinsicGeometry.I3, interior_range_modelWithCornersEuclideanHalfSpace, mem_ofPred_eq] using hpos apply hnot apply (OAI.CKSIntrinsicGeometry.I3.isInteriorPoint_iff_of_mem_atlas one_ne_zero (chart_mem_atlas OAI.CKSIntrinsicGeometry.H3 x) hychart).mpr exact (chartAt OAI.CKSIntrinsicGeometry.H3 x).mem_interior_extend_target ((chartAt OAI.CKSIntrinsicGeometry.H3 x).map_source hychart) hint exact le_antisymm hle hnonneg have proof_liftPlane_zero_6 (z : OAI.CKSBoundarySurface.E2) : OAI.CKSBoundarySurface.liftPlane z 0 = 0 := rfl have proof_liftPlane_succ_7 (z : OAI.CKSBoundarySurface.E2) (i : Fin 2) : OAI.CKSBoundarySurface.liftPlane z i.succ = z i := rfl have proof_I3_liftHalf_23 (z : OAI.CKSBoundarySurface.E2) : OAI.CKSBoundarySurface.I3 (OAI.CKSBoundarySurface.liftHalf z) = OAI.CKSBoundarySurface.liftPlane z := rfl have proof_boundary_iff_zero_24 {M : Type u_1} [instLocal1 : TopologicalSpace.{u_1} M] [instLocal2 : ChartedSpace.{0, u_1} OAI.CKSBoundarySurface.H3 M] [instLocal3 : IsManifold.{0, 0, 0, u_1} OAI.CKSBoundarySurface.I3 (∞ : ℕ∞ω) M] (x y : M) (hy : y ∈ (chartAt OAI.CKSBoundarySurface.H3 x).source) : y ∈ OAI.CKSBoundarySurface.I3.boundary M ↔ (OAI.CKSBoundarySurface.I3 (chartAt OAI.CKSBoundarySurface.H3 x y)) 0 = 0 := by constructor · exact proof_boundary_chart_zero_22 x y (by simp [*]) · intro hz apply (OAI.CKSBoundarySurface.I3.isBoundaryPoint_iff_not_isInteriorPoint y).mpr intro hi have hin := (OAI.CKSBoundarySurface.I3.isInteriorPoint_iff_of_mem_atlas (by simp [*] : (∞ : ℕ∞ω) ≠ 0) (chart_mem_atlas OAI.CKSBoundarySurface.H3 x) hy).mp hi have hr := (chartAt OAI.CKSBoundarySurface.H3 x).interior_extend_target_subset_interior_range hin have hp : 0 < (OAI.CKSBoundarySurface.I3 (chartAt OAI.CKSBoundarySurface.H3 x y)) 0 := by simpa only [OAI.CKSBoundarySurface.I3, interior_range_modelWithCornersEuclideanHalfSpace, mem_ofPred_eq, OpenPartialHomeomorph.extend_coe, Function.comp_apply] using hr rw [hz] at hp exact (lt_irrefl 0) hp have proof_chart_inverse_boundary_25 {M : Type u_1} [instLocal1 : TopologicalSpace.{u_1} M] [instLocal2 : ChartedSpace.{0, u_1} OAI.CKSBoundarySurface.H3 M] [instLocal3 : IsManifold.{0, 0, 0, u_1} OAI.CKSBoundarySurface.I3 (∞ : ℕ∞ω) M] (x : M) {z : OAI.CKSBoundarySurface.E2} (hz : OAI.CKSBoundarySurface.liftHalf z ∈ (chartAt OAI.CKSBoundarySurface.H3 x).target) : (chartAt OAI.CKSBoundarySurface.H3 x).symm (OAI.CKSBoundarySurface.liftHalf z) ∈ OAI.CKSBoundarySurface.I3.boundary M := by apply (proof_boundary_iff_zero_24 x _ ((chartAt OAI.CKSBoundarySurface.H3 x).map_target hz)).mpr rw [(chartAt OAI.CKSBoundarySurface.H3 x).right_inv hz] rfl have proof_boundaryInverse_mem_21 {M : Type u_1} [instLocal1 : TopologicalSpace.{u_1} M] [instLocal2 : ChartedSpace.{0, u_1} OAI.CKSBoundarySurface.H3 M] [instLocal3 : IsManifold.{0, 0, 0, u_1} OAI.CKSBoundarySurface.I3 (∞ : ℕ∞ω) M] (x : OAI.CKSBoundarySurface.Boundary M) {z : OAI.CKSBoundarySurface.E2} (hz : OAI.CKSBoundarySurface.liftHalf z ∈ (chartAt OAI.CKSBoundarySurface.H3 x.val).target) : (chartAt OAI.CKSBoundarySurface.H3 x.val).symm (OAI.CKSBoundarySurface.liftHalf z) ∈ OAI.CKSBoundarySurface.Boundary M := proof_chart_inverse_boundary_25 x.val hz if hz : OAI.CKSBoundarySurface.liftHalf z ∈ (chartAt OAI.CKSBoundarySurface.H3 x.val).target then ⟨(chartAt OAI.CKSBoundarySurface.H3 x.val).symm (OAI.CKSBoundarySurface.liftHalf z),proof_boundaryInverse_mem_21 x hz⟩ else xdef boundaryChart (x : OAI.CKSBoundarySurface.Boundary M) : OpenPartialHomeomorph (OAI.CKSBoundarySurface.Boundary M) OAI.CKSBoundarySurface.E2 := have proof_lift_drop_30 {z : OAI.CKSBoundarySurface.E3} (hz : z 0 = 0) : OAI.CKSBoundarySurface.liftPlane (OAI.CKSBoundarySurface.dropPlane z) = z := by ext i cases i using Fin.cases with | zero => exact hz.symm | succ i => rfl have proof_boundary_chart_zero_22 {M : Type u_1} [instLocal1 : TopologicalSpace.{u_1} M] [instLocal2 : ChartedSpace.{0, u_1} OAI.CKSIntrinsicGeometry.H3 M] [instLocal3 : IsManifold.{0, 0, 0, u_1} OAI.CKSIntrinsicGeometry.I3 1 M] (x y : M) (hy : y ∈ (extChartAt OAI.CKSIntrinsicGeometry.I3 x).source) (hS : y ∈ OAI.CKSIntrinsicGeometry.I3.boundary M) : (extChartAt OAI.CKSIntrinsicGeometry.I3 x y) 0 = 0 := by have hychart : y ∈ (chartAt OAI.CKSIntrinsicGeometry.H3 x).source := by simpa using hy have hyrange : extChartAt OAI.CKSIntrinsicGeometry.I3 x y ∈ range OAI.CKSIntrinsicGeometry.I3 := (extChartAt_target_subset_range x) ((extChartAt OAI.CKSIntrinsicGeometry.I3 x).map_source hy) have hnonneg : 0 ≤ (extChartAt OAI.CKSIntrinsicGeometry.I3 x y) 0 := by simpa only [OAI.CKSIntrinsicGeometry.I3, range_modelWithCornersEuclideanHalfSpace, mem_ofPred_eq] using hyrange have hnot : ¬OAI.CKSIntrinsicGeometry.I3.IsInteriorPoint y := (OAI.CKSIntrinsicGeometry.I3.isBoundaryPoint_iff_not_isInteriorPoint y).mp hS have hle : (extChartAt OAI.CKSIntrinsicGeometry.I3 x y) 0 ≤ 0 := by by_contra h have hpos : 0 < (extChartAt OAI.CKSIntrinsicGeometry.I3 x y) 0 := lt_of_not_ge h have hint : extChartAt OAI.CKSIntrinsicGeometry.I3 x y ∈ interior (range OAI.CKSIntrinsicGeometry.I3) := by simpa only [OAI.CKSIntrinsicGeometry.I3, interior_range_modelWithCornersEuclideanHalfSpace, mem_ofPred_eq] using hpos apply hnot apply (OAI.CKSIntrinsicGeometry.I3.isInteriorPoint_iff_of_mem_atlas one_ne_zero (chart_mem_atlas OAI.CKSIntrinsicGeometry.H3 x) hychart).mpr exact (chartAt OAI.CKSIntrinsicGeometry.H3 x).mem_interior_extend_target ((chartAt OAI.CKSIntrinsicGeometry.H3 x).map_source hychart) hint exact le_antisymm hle hnonneg have proof_liftPlane_zero_6 (z : OAI.CKSBoundarySurface.E2) : OAI.CKSBoundarySurface.liftPlane z 0 = 0 := rfl have proof_liftPlane_succ_7 (z : OAI.CKSBoundarySurface.E2) (i : Fin 2) : OAI.CKSBoundarySurface.liftPlane z i.succ = z i := rfl have proof_I3_liftHalf_23 (z : OAI.CKSBoundarySurface.E2) : OAI.CKSBoundarySurface.I3 (OAI.CKSBoundarySurface.liftHalf z) = OAI.CKSBoundarySurface.liftPlane z := rfl have proof_boundary_iff_zero_24 {M : Type u_1} [instLocal1 : TopologicalSpace.{u_1} M] [instLocal2 : ChartedSpace.{0, u_1} OAI.CKSBoundarySurface.H3 M] [instLocal3 : IsManifold.{0, 0, 0, u_1} OAI.CKSBoundarySurface.I3 (∞ : ℕ∞ω) M] (x y : M) (hy : y ∈ (chartAt OAI.CKSBoundarySurface.H3 x).source) : y ∈ OAI.CKSBoundarySurface.I3.boundary M ↔ (OAI.CKSBoundarySurface.I3 (chartAt OAI.CKSBoundarySurface.H3 x y)) 0 = 0 := by constructor · exact proof_boundary_chart_zero_22 x y (by simp [*]) · intro hz apply (OAI.CKSBoundarySurface.I3.isBoundaryPoint_iff_not_isInteriorPoint y).mpr intro hi have hin := (OAI.CKSBoundarySurface.I3.isInteriorPoint_iff_of_mem_atlas (by simp [*] : (∞ : ℕ∞ω) ≠ 0) (chart_mem_atlas OAI.CKSBoundarySurface.H3 x) hy).mp hi have hr := (chartAt OAI.CKSBoundarySurface.H3 x).interior_extend_target_subset_interior_range hin have hp : 0 < (OAI.CKSBoundarySurface.I3 (chartAt OAI.CKSBoundarySurface.H3 x y)) 0 := by simpa only [OAI.CKSBoundarySurface.I3, interior_range_modelWithCornersEuclideanHalfSpace, mem_ofPred_eq, OpenPartialHomeomorph.extend_coe, Function.comp_apply] using hr rw [hz] at hp exact (lt_irrefl 0) hp have proof_liftHalf_drop_chart_26 {M : Type u_1} [instLocal1 : TopologicalSpace.{u_1} M] [instLocal2 : ChartedSpace.{0, u_1} OAI.CKSBoundarySurface.H3 M] [instLocal3 : IsManifold.{0, 0, 0, u_1} OAI.CKSBoundarySurface.I3 (∞ : ℕ∞ω) M] (x : M) (y : OAI.CKSBoundarySurface.Boundary M) (hy : y.val ∈ (chartAt OAI.CKSBoundarySurface.H3 x).source) : OAI.CKSBoundarySurface.liftHalf (OAI.CKSBoundarySurface.dropPlane (OAI.CKSBoundarySurface.I3 (chartAt OAI.CKSBoundarySurface.H3 x y.val))) = chartAt OAI.CKSBoundarySurface.H3 x y.val := by apply Subtype.ext exact proof_lift_drop_30 ((proof_boundary_iff_zero_24 x y.val hy).mp y.property) have proof_chart_inverse_boundary_25 {M : Type u_1} [instLocal1 : TopologicalSpace.{u_1} M] [instLocal2 : ChartedSpace.{0, u_1} OAI.CKSBoundarySurface.H3 M] [instLocal3 : IsManifold.{0, 0, 0, u_1} OAI.CKSBoundarySurface.I3 (∞ : ℕ∞ω) M] (x : M) {z : OAI.CKSBoundarySurface.E2} (hz : OAI.CKSBoundarySurface.liftHalf z ∈ (chartAt OAI.CKSBoundarySurface.H3 x).target) : (chartAt OAI.CKSBoundarySurface.H3 x).symm (OAI.CKSBoundarySurface.liftHalf z) ∈ OAI.CKSBoundarySurface.I3.boundary M := by apply (proof_boundary_iff_zero_24 x _ ((chartAt OAI.CKSBoundarySurface.H3 x).map_target hz)).mpr rw [(chartAt OAI.CKSBoundarySurface.H3 x).right_inv hz] rfl have proof_boundaryInverse_mem_21 {M : Type u_1} [instLocal1 : TopologicalSpace.{u_1} M] [instLocal2 : ChartedSpace.{0, u_1} OAI.CKSBoundarySurface.H3 M] [instLocal3 : IsManifold.{0, 0, 0, u_1} OAI.CKSBoundarySurface.I3 (∞ : ℕ∞ω) M] (x : OAI.CKSBoundarySurface.Boundary M) {z : OAI.CKSBoundarySurface.E2} (hz : OAI.CKSBoundarySurface.liftHalf z ∈ (chartAt OAI.CKSBoundarySurface.H3 x.val).target) : (chartAt OAI.CKSBoundarySurface.H3 x.val).symm (OAI.CKSBoundarySurface.liftHalf z) ∈ OAI.CKSBoundarySurface.Boundary M := proof_chart_inverse_boundary_25 x.val hz have proof_boundaryInverse_val_27 {M : Type u_1} [instLocal1 : TopologicalSpace.{u_1} M] [instLocal2 : ChartedSpace.{0, u_1} OAI.CKSBoundarySurface.H3 M] [instLocal3 : IsManifold.{0, 0, 0, u_1} OAI.CKSBoundarySurface.I3 (∞ : ℕ∞ω) M] (x : OAI.CKSBoundarySurface.Boundary M) {z : OAI.CKSBoundarySurface.E2} (hz : OAI.CKSBoundarySurface.liftHalf z ∈ (chartAt OAI.CKSBoundarySurface.H3 x.val).target) : (OAI.CKSBoundarySurface.boundaryInverse x z).val = (chartAt OAI.CKSBoundarySurface.H3 x.val).symm (OAI.CKSBoundarySurface.liftHalf z) := by simp only [OAI.CKSBoundarySurface.boundaryInverse,dite_eq_left hz] have proof_dropPlane_apply_31 (z : OAI.CKSBoundarySurface.E3) (i : Fin 2) : OAI.CKSBoundarySurface.dropPlane z i = z i.succ := rfl have proof_drop_lift_28 (z : OAI.CKSBoundarySurface.E2) : OAI.CKSBoundarySurface.dropPlane (OAI.CKSBoundarySurface.liftPlane z) = z := by ext i; rfl have proof_liftHalf_continuous_29 : Continuous OAI.CKSBoundarySurface.liftHalf := OAI.CKSBoundarySurface.liftPlane.continuous.subtype_mk (fun _ => by simp [*]) { toFun y := OAI.CKSBoundarySurface.dropPlane (OAI.CKSBoundarySurface.I3 (chartAt OAI.CKSBoundarySurface.H3 x.val y.val)) invFun := OAI.CKSBoundarySurface.boundaryInverse x source := Subtype.val ⁻¹' (chartAt OAI.CKSBoundarySurface.H3 x.val).source target := OAI.CKSBoundarySurface.liftHalf ⁻¹' (chartAt OAI.CKSBoundarySurface.H3 x.val).target map_source' := by intro y hy change OAI.CKSBoundarySurface.liftHalf (OAI.CKSBoundarySurface.dropPlane (OAI.CKSBoundarySurface.I3 (chartAt OAI.CKSBoundarySurface.H3 x.val y.val))) ∈ (chartAt OAI.CKSBoundarySurface.H3 x.val).target rw [proof_liftHalf_drop_chart_26 x.val y hy] exact (chartAt OAI.CKSBoundarySurface.H3 x.val).map_source hy map_target' := by intro z hz change (OAI.CKSBoundarySurface.boundaryInverse x z).val ∈ (chartAt OAI.CKSBoundarySurface.H3 x.val).source rw [proof_boundaryInverse_val_27 x hz] exact (chartAt OAI.CKSBoundarySurface.H3 x.val).map_target hz left_inv' := by intro y hy have h := proof_liftHalf_drop_chart_26 x.val y hy apply Subtype.ext rw [proof_boundaryInverse_val_27 x (by rw [h]; exact (chartAt OAI.CKSBoundarySurface.H3 x.val).map_source hy),h] exact (chartAt OAI.CKSBoundarySurface.H3 x.val).left_inv hy right_inv' := by intro z hz rw [proof_boundaryInverse_val_27 x hz,(chartAt OAI.CKSBoundarySurface.H3 x.val).right_inv hz,proof_I3_liftHalf_23,proof_drop_lift_28] open_source := (chartAt OAI.CKSBoundarySurface.H3 x.val).open_source.preimage continuous_subtype_val open_target := (chartAt OAI.CKSBoundarySurface.H3 x.val).open_target.preimage proof_liftHalf_continuous_29 continuousOn_toFun := OAI.CKSBoundarySurface.dropPlane.continuous.comp_continuousOn (OAI.CKSBoundarySurface.I3.continuous.comp_continuousOn ((chartAt OAI.CKSBoundarySurface.H3 x.val).continuousOn.comp continuous_subtype_val.continuousOn (fun _ h => h))) continuousOn_invFun := by apply Topology.IsInducing.subtypeVal.continuousOn_iff.mpr apply ((chartAt OAI.CKSBoundarySurface.H3 x.val).continuousOn_symm.comp proof_liftHalf_continuous_29.continuousOn (fun _ h => h)).congr intro z hz exact proof_boundaryInverse_val_27 x hz }instance boundaryChartedSpace : ChartedSpace OAI.CKSBoundarySurface.E2 (OAI.CKSBoundarySurface.Boundary M) where atlas := range OAI.CKSBoundarySurface.boundaryChart chartAt := OAI.CKSBoundarySurface.boundaryChart mem_chart_source x := mem_chart_source OAI.CKSBoundarySurface.H3 x.val chart_mem_atlas x := mem_range_self xend OAI.CKSBoundarySurfaceendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSBoundarySurfaceopen Set Manifold Bundle Filter Functionopen scoped ContDiff Topologyvariable {M : Type u_1} [TopologicalSpace M] [ChartedSpace H3 M] [IsManifold I3 ∞ M]instance boundaryIsManifold : IsManifold OAI.CKSBoundarySurface.I2 ∞ (OAI.CKSBoundarySurface.Boundary M) := have proof_lift_mem_ext_target_34 {M : Type u_1} [instLocal1 : TopologicalSpace.{u_1} M] [instLocal2 : ChartedSpace.{0, u_1} OAI.CKSBoundarySurface.H3 M] [instLocal3 : IsManifold.{0, 0, 0, u_1} OAI.CKSBoundarySurface.I3 (∞ : ℕ∞ω) M] [IsManifold OAI.CKSBoundarySurface.I3 ∞ M] (x : M) {z : OAI.CKSBoundarySurface.E2} (hz : OAI.CKSBoundarySurface.liftHalf z ∈ (chartAt OAI.CKSBoundarySurface.H3 x).target) : OAI.CKSBoundarySurface.liftPlane z ∈ (extChartAt OAI.CKSBoundarySurface.I3 x).target := by change OAI.CKSBoundarySurface.liftPlane z ∈ ((chartAt OAI.CKSBoundarySurface.H3 x).extend OAI.CKSBoundarySurface.I3).target rw [OpenPartialHomeomorph.extend_target'] exact ⟨OAI.CKSBoundarySurface.liftHalf z,hz,rfl⟩ have proof_ext_symm_lift_35 {M : Type u_1} [instLocal1 : TopologicalSpace.{u_1} M] [instLocal2 : ChartedSpace.{0, u_1} OAI.CKSBoundarySurface.H3 M] [instLocal3 : IsManifold.{0, 0, 0, u_1} OAI.CKSBoundarySurface.I3 (∞ : ℕ∞ω) M] [IsManifold OAI.CKSBoundarySurface.I3 ∞ M] (x : M) (z : OAI.CKSBoundarySurface.E2) : (extChartAt OAI.CKSBoundarySurface.I3 x).symm (OAI.CKSBoundarySurface.liftPlane z) = (chartAt OAI.CKSBoundarySurface.H3 x).symm (OAI.CKSBoundarySurface.liftHalf z) := by change (chartAt OAI.CKSBoundarySurface.H3 x).symm (OAI.CKSBoundarySurface.I3.symm (OAI.CKSBoundarySurface.I3 (OAI.CKSBoundarySurface.liftHalf z))) = _ rw [OAI.CKSBoundarySurface.I3.left_inv] have proof_boundary_chart_zero_22 {M : Type u_1} [instLocal1 : TopologicalSpace.{u_1} M] [instLocal2 : ChartedSpace.{0, u_1} OAI.CKSIntrinsicGeometry.H3 M] [instLocal3 : IsManifold.{0, 0, 0, u_1} OAI.CKSIntrinsicGeometry.I3 1 M] (x y : M) (hy : y ∈ (extChartAt OAI.CKSIntrinsicGeometry.I3 x).source) (hS : y ∈ OAI.CKSIntrinsicGeometry.I3.boundary M) : (extChartAt OAI.CKSIntrinsicGeometry.I3 x y) 0 = 0 := by have hychart : y ∈ (chartAt OAI.CKSIntrinsicGeometry.H3 x).source := by simpa using hy have hyrange : extChartAt OAI.CKSIntrinsicGeometry.I3 x y ∈ range OAI.CKSIntrinsicGeometry.I3 := (extChartAt_target_subset_range x) ((extChartAt OAI.CKSIntrinsicGeometry.I3 x).map_source hy) have hnonneg : 0 ≤ (extChartAt OAI.CKSIntrinsicGeometry.I3 x y) 0 := by simpa only [OAI.CKSIntrinsicGeometry.I3, range_modelWithCornersEuclideanHalfSpace, mem_ofPred_eq] using hyrange have hnot : ¬OAI.CKSIntrinsicGeometry.I3.IsInteriorPoint y := (OAI.CKSIntrinsicGeometry.I3.isBoundaryPoint_iff_not_isInteriorPoint y).mp hS have hle : (extChartAt OAI.CKSIntrinsicGeometry.I3 x y) 0 ≤ 0 := by by_contra h have hpos : 0 < (extChartAt OAI.CKSIntrinsicGeometry.I3 x y) 0 := lt_of_not_ge h have hint : extChartAt OAI.CKSIntrinsicGeometry.I3 x y ∈ interior (range OAI.CKSIntrinsicGeometry.I3) := by simpa only [OAI.CKSIntrinsicGeometry.I3, interior_range_modelWithCornersEuclideanHalfSpace, mem_ofPred_eq] using hpos apply hnot apply (OAI.CKSIntrinsicGeometry.I3.isInteriorPoint_iff_of_mem_atlas one_ne_zero (chart_mem_atlas OAI.CKSIntrinsicGeometry.H3 x) hychart).mpr exact (chartAt OAI.CKSIntrinsicGeometry.H3 x).mem_interior_extend_target ((chartAt OAI.CKSIntrinsicGeometry.H3 x).map_source hychart) hint exact le_antisymm hle hnonneg have proof_liftPlane_zero_6 (z : OAI.CKSBoundarySurface.E2) : OAI.CKSBoundarySurface.liftPlane z 0 = 0 := rfl have proof_liftPlane_succ_7 (z : OAI.CKSBoundarySurface.E2) (i : Fin 2) : OAI.CKSBoundarySurface.liftPlane z i.succ = z i := rfl have proof_I3_liftHalf_23 (z : OAI.CKSBoundarySurface.E2) : OAI.CKSBoundarySurface.I3 (OAI.CKSBoundarySurface.liftHalf z) = OAI.CKSBoundarySurface.liftPlane z := rfl have proof_boundary_iff_zero_24 {M : Type u_1} [instLocal1 : TopologicalSpace.{u_1} M] [instLocal2 : ChartedSpace.{0, u_1} OAI.CKSBoundarySurface.H3 M] [instLocal3 : IsManifold.{0, 0, 0, u_1} OAI.CKSBoundarySurface.I3 (∞ : ℕ∞ω) M] (x y : M) (hy : y ∈ (chartAt OAI.CKSBoundarySurface.H3 x).source) : y ∈ OAI.CKSBoundarySurface.I3.boundary M ↔ (OAI.CKSBoundarySurface.I3 (chartAt OAI.CKSBoundarySurface.H3 x y)) 0 = 0 := by constructor · exact proof_boundary_chart_zero_22 x y (by simp [*]) · intro hz apply (OAI.CKSBoundarySurface.I3.isBoundaryPoint_iff_not_isInteriorPoint y).mpr intro hi have hin := (OAI.CKSBoundarySurface.I3.isInteriorPoint_iff_of_mem_atlas (by simp [*] : (∞ : ℕ∞ω) ≠ 0) (chart_mem_atlas OAI.CKSBoundarySurface.H3 x) hy).mp hi have hr := (chartAt OAI.CKSBoundarySurface.H3 x).interior_extend_target_subset_interior_range hin have hp : 0 < (OAI.CKSBoundarySurface.I3 (chartAt OAI.CKSBoundarySurface.H3 x y)) 0 := by simpa only [OAI.CKSBoundarySurface.I3, interior_range_modelWithCornersEuclideanHalfSpace, mem_ofPred_eq, OpenPartialHomeomorph.extend_coe, Function.comp_apply] using hr rw [hz] at hp exact (lt_irrefl 0) hp have proof_chart_inverse_boundary_25 {M : Type u_1} [instLocal1 : TopologicalSpace.{u_1} M] [instLocal2 : ChartedSpace.{0, u_1} OAI.CKSBoundarySurface.H3 M] [instLocal3 : IsManifold.{0, 0, 0, u_1} OAI.CKSBoundarySurface.I3 (∞ : ℕ∞ω) M] (x : M) {z : OAI.CKSBoundarySurface.E2} (hz : OAI.CKSBoundarySurface.liftHalf z ∈ (chartAt OAI.CKSBoundarySurface.H3 x).target) : (chartAt OAI.CKSBoundarySurface.H3 x).symm (OAI.CKSBoundarySurface.liftHalf z) ∈ OAI.CKSBoundarySurface.I3.boundary M := by apply (proof_boundary_iff_zero_24 x _ ((chartAt OAI.CKSBoundarySurface.H3 x).map_target hz)).mpr rw [(chartAt OAI.CKSBoundarySurface.H3 x).right_inv hz] rfl have proof_boundaryInverse_mem_21 {M : Type u_1} [instLocal1 : TopologicalSpace.{u_1} M] [instLocal2 : ChartedSpace.{0, u_1} OAI.CKSBoundarySurface.H3 M] [instLocal3 : IsManifold.{0, 0, 0, u_1} OAI.CKSBoundarySurface.I3 (∞ : ℕ∞ω) M] (x : OAI.CKSBoundarySurface.Boundary M) {z : OAI.CKSBoundarySurface.E2} (hz : OAI.CKSBoundarySurface.liftHalf z ∈ (chartAt OAI.CKSBoundarySurface.H3 x.val).target) : (chartAt OAI.CKSBoundarySurface.H3 x.val).symm (OAI.CKSBoundarySurface.liftHalf z) ∈ OAI.CKSBoundarySurface.Boundary M := proof_chart_inverse_boundary_25 x.val hz have proof_boundaryInverse_val_27 {M : Type u_1} [instLocal1 : TopologicalSpace.{u_1} M] [instLocal2 : ChartedSpace.{0, u_1} OAI.CKSBoundarySurface.H3 M] [instLocal3 : IsManifold.{0, 0, 0, u_1} OAI.CKSBoundarySurface.I3 (∞ : ℕ∞ω) M] (x : OAI.CKSBoundarySurface.Boundary M) {z : OAI.CKSBoundarySurface.E2} (hz : OAI.CKSBoundarySurface.liftHalf z ∈ (chartAt OAI.CKSBoundarySurface.H3 x.val).target) : (OAI.CKSBoundarySurface.boundaryInverse x z).val = (chartAt OAI.CKSBoundarySurface.H3 x.val).symm (OAI.CKSBoundarySurface.liftHalf z) := by simp only [OAI.CKSBoundarySurface.boundaryInverse,dite_eq_left hz] have proof_boundaryChart_symm_val_36 {M : Type u_1} [instLocal1 : TopologicalSpace.{u_1} M] [instLocal2 : ChartedSpace.{0, u_1} OAI.CKSBoundarySurface.H3 M] [instLocal3 : IsManifold.{0, 0, 0, u_1} OAI.CKSBoundarySurface.I3 (∞ : ℕ∞ω) M] (x : OAI.CKSBoundarySurface.Boundary M) {z : OAI.CKSBoundarySurface.E2} (hz : z ∈ (OAI.CKSBoundarySurface.boundaryChart x).target) : ((OAI.CKSBoundarySurface.boundaryChart x).symm z).val = (chartAt OAI.CKSBoundarySurface.H3 x.val).symm (OAI.CKSBoundarySurface.liftHalf z) := proof_boundaryInverse_val_27 x hz have proof_transition_lift_maps_32 {M : Type u_1} [instLocal1 : TopologicalSpace.{u_1} M] [instLocal2 : ChartedSpace.{0, u_1} OAI.CKSBoundarySurface.H3 M] [instLocal3 : IsManifold.{0, 0, 0, u_1} OAI.CKSBoundarySurface.I3 (∞ : ℕ∞ω) M] (x y : OAI.CKSBoundarySurface.Boundary M) : MapsTo OAI.CKSBoundarySurface.liftPlane ((OAI.CKSBoundarySurface.boundaryChart x).symm ≫ₕ OAI.CKSBoundarySurface.boundaryChart y).source ((extChartAt OAI.CKSBoundarySurface.I3 x.val).symm ≫ extChartAt OAI.CKSBoundarySurface.I3 y.val).source := by intro z hz change z ∈ (OAI.CKSBoundarySurface.boundaryChart x).target ∧ (OAI.CKSBoundarySurface.boundaryChart x).symm z ∈ (OAI.CKSBoundarySurface.boundaryChart y).source at hz refine ⟨proof_lift_mem_ext_target_34 x.val hz.1, ?_⟩ change (extChartAt OAI.CKSBoundarySurface.I3 x.val).symm (OAI.CKSBoundarySurface.liftPlane z) ∈ (extChartAt OAI.CKSBoundarySurface.I3 y.val).source rw [proof_ext_symm_lift_35] have h := hz.2 change ((OAI.CKSBoundarySurface.boundaryChart x).symm z).val ∈ (chartAt OAI.CKSBoundarySurface.H3 y.val).source at h rw [proof_boundaryChart_symm_val_36 x hz.1] at h simpa only [extChartAt_source] using h have proof_transition_formula_33 {M : Type u_1} [instLocal1 : TopologicalSpace.{u_1} M] [instLocal2 : ChartedSpace.{0, u_1} OAI.CKSBoundarySurface.H3 M] [instLocal3 : IsManifold.{0, 0, 0, u_1} OAI.CKSBoundarySurface.I3 (∞ : ℕ∞ω) M] (x y : OAI.CKSBoundarySurface.Boundary M) {z : OAI.CKSBoundarySurface.E2} (hz : z ∈ ((OAI.CKSBoundarySurface.boundaryChart x).symm ≫ₕ OAI.CKSBoundarySurface.boundaryChart y).source) : ((OAI.CKSBoundarySurface.boundaryChart x).symm ≫ₕ OAI.CKSBoundarySurface.boundaryChart y) z = OAI.CKSBoundarySurface.dropPlane (((extChartAt OAI.CKSBoundarySurface.I3 x.val).symm ≫ extChartAt OAI.CKSBoundarySurface.I3 y.val) (OAI.CKSBoundarySurface.liftPlane z)) := by change OAI.CKSBoundarySurface.dropPlane (OAI.CKSBoundarySurface.I3 (chartAt OAI.CKSBoundarySurface.H3 y.val ((OAI.CKSBoundarySurface.boundaryChart x).symm z).val)) = _ rw [proof_boundaryChart_symm_val_36 x hz.1] change _ = OAI.CKSBoundarySurface.dropPlane (OAI.CKSBoundarySurface.I3 (chartAt OAI.CKSBoundarySurface.H3 y.val ((extChartAt OAI.CKSBoundarySurface.I3 x.val).symm (OAI.CKSBoundarySurface.liftPlane z)))) rw [proof_ext_symm_lift_35] by apply isManifold_of_contDiffOn rintro e e' ⟨x,rfl⟩ ⟨y,rfl⟩ change ContDiffOn ℝ ∞ (fun z => ((OAI.CKSBoundarySurface.boundaryChart x).symm ≫ₕ OAI.CKSBoundarySurface.boundaryChart y) z) (id ⁻¹' ((OAI.CKSBoundarySurface.boundaryChart x).symm ≫ₕ OAI.CKSBoundarySurface.boundaryChart y).source ∩ range id) rw [preimage_id,range_id,inter_univ] apply (OAI.CKSBoundarySurface.dropPlane.contDiff.comp_contDiffOn ((contDiffOn_ext_coord_change (I := OAI.CKSBoundarySurface.I3) y.val x.val).comp OAI.CKSBoundarySurface.liftPlane.contDiff.contDiffOn (proof_transition_lift_maps_32 x y))).congr intro z hz exact proof_transition_formula_33 x y hzend OAI.CKSBoundarySurfaceendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSSurfaceVolumeopen Bundle Manifold Set MeasureTheoryopen scoped ContDiff ENNRealabbrev E := EuclideanSpace ℝ (Fin 2)abbrev H := OAI.CKSSurfaceVolume.Eabbrev I := 𝓘(ℝ,OAI.CKSSurfaceVolume.E)abbrev basis (i : Fin 2) : OAI.CKSSurfaceVolume.E := EuclideanSpace.single i 1end OAI.CKSSurfaceVolumeendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSSurfaceVolumeopen Bundle Manifold Set MeasureTheoryopen scoped ContDiff ENNRealvariable {M : Type u_1} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M]abbrev Metric := ContinuousRiemannianMetric OAI.CKSSurfaceVolume.E (fun x : M => TangentSpace OAI.CKSSurfaceVolume.I x)end OAI.CKSSurfaceVolumeendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSSurfaceVolumeopen Bundle Manifold Set MeasureTheoryopen scoped ContDiff ENNRealvariable {M : Type*} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M]local instance real_continuousAdd : ContinuousAdd ℝ := inferInstancelocal instance real_continuousConstSMul : ContinuousConstSMul ℝ ℝ := inferInstancelocal instance real_smulCommClass : @SMulCommClass ℝ ℝ ℝ Algebra.toSMul (@instSMulOfMul ℝ (@Distrib.toMul ℝ (@instDistribOfSemiring ℝ (@CommSemiring.toSemiring ℝ Real.instCommSemiring)))) := inferInstanceend OAI.CKSSurfaceVolumeendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSSurfaceVolumeopen Bundle Manifold Set MeasureTheoryopen scoped ContDiff ENNRealvariable {M : Type u_1} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M]def chartFrame (x : M) (y : OAI.CKSSurfaceVolume.E) : OAI.CKSSurfaceVolume.E →L[ℝ] TangentSpace OAI.CKSSurfaceVolume.I ((extChartAt OAI.CKSSurfaceVolume.I x).symm y) := mfderivWithin 𝓘(ℝ,OAI.CKSSurfaceVolume.E) OAI.CKSSurfaceVolume.I (extChartAt OAI.CKSSurfaceVolume.I x).symm (range OAI.CKSSurfaceVolume.I) ydef chartMatrix (g : OAI.CKSSurfaceVolume.Metric (M := M)) (x : M) (y : OAI.CKSSurfaceVolume.E) : Matrix (Fin 2) (Fin 2) ℝ := letI := OAI.CKSSurfaceVolume.real_continuousAdd letI := OAI.CKSSurfaceVolume.real_continuousConstSMul letI := OAI.CKSSurfaceVolume.real_smulCommClass let inner : TangentSpace OAI.CKSSurfaceVolume.I ((extChartAt OAI.CKSSurfaceVolume.I x).symm y) →L[ℝ] TangentSpace OAI.CKSSurfaceVolume.I ((extChartAt OAI.CKSSurfaceVolume.I x).symm y) →L[ℝ] ℝ := g.inner ((extChartAt OAI.CKSSurfaceVolume.I x).symm y) fun i j => inner (OAI.CKSSurfaceVolume.chartFrame x y (OAI.CKSSurfaceVolume.basis i)) (OAI.CKSSurfaceVolume.chartFrame x y (OAI.CKSSurfaceVolume.basis j))def chartDensity (g : OAI.CKSSurfaceVolume.Metric (M := M)) (x : M) (y : OAI.CKSSurfaceVolume.E) : ℝ := Real.sqrt (OAI.CKSSurfaceVolume.chartMatrix g x y).detend OAI.CKSSurfaceVolumeendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSSurfaceVolumeopen Bundle Manifold Set MeasureTheoryopen scoped ContDiff ENNRealvariable {M : Type u_1} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M]variable [MeasurableSpace M] [BorelSpace M]def localVolume (g : OAI.CKSSurfaceVolume.Metric (M := M)) (x : M) : Measure M := Measure.map (extChartAt OAI.CKSSurfaceVolume.I x).symm ((volume.restrict (extChartAt OAI.CKSSurfaceVolume.I x).target).withDensity (fun y => ENNReal.ofReal (OAI.CKSSurfaceVolume.chartDensity g x y)))def IsVolume (g : OAI.CKSSurfaceVolume.Metric (M := M)) (ν : Measure M) : Prop := ∀ x : M, ν.restrict (extChartAt OAI.CKSSurfaceVolume.I x).source = OAI.CKSSurfaceVolume.localVolume g xend OAI.CKSSurfaceVolumeendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSSurfaceVolumeopen Bundle Manifold Set MeasureTheoryopen scoped ContDiff ENNRealdef riemannianVolume {M : Type u_1} [TopologicalSpace M] [ChartedSpace OAI.CKSSurfaceVolume.H M] [IsManifold OAI.CKSSurfaceVolume.I 1 M] [MeasurableSpace M] [BorelSpace M] [SecondCountableTopology M] (g : OAI.CKSSurfaceVolume.Metric (M := M)) : Measure M := Classical.epsilon (fun ν => OAI.CKSSurfaceVolume.IsVolume g ν)end OAI.CKSSurfaceVolumeendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSInducedAreaopen Bundle Manifold Set Bornology Filteropen scoped Bundle Manifold ContDiff Topologyabbrev E2 := EuclideanSpace ℝ (Fin 2)abbrev I2 := 𝓘(ℝ,OAI.CKSInducedArea.E2)abbrev E3 := EuclideanSpace ℝ (Fin 3)end OAI.CKSInducedAreaendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSInducedAreaopen Bundle Manifold Set Bornology Filteropen scoped Bundle Manifold ContDiff Topologyvariable {H3 : Type*} [TopologicalSpace H3] {I3 : ModelWithCorners ℝ E3 H3} {N : Type*} [TopologicalSpace N] [ChartedSpace H3 N] [IsManifold I3 ∞ N] {S : Type*} [TopologicalSpace S] [ChartedSpace E2 S] [IsManifold I2 ∞ S]local instance real_continuousAdd : ContinuousAdd ℝ := inferInstancelocal instance real_continuousConstSMul : ContinuousConstSMul ℝ ℝ := inferInstancelocal instance real_id_isometric : RingHomIsometric (RingHom.id ℝ) := inferInstancelocal instance real_id_compTriple : RingHomCompTriple (RingHom.id ℝ) (RingHom.id ℝ) (RingHom.id ℝ) := inferInstancelocal instance real_smulCommClass : @SMulCommClass ℝ ℝ ℝ Algebra.toSMul (@instSMulOfMul ℝ (@Distrib.toMul ℝ (@instDistribOfSemiring ℝ (@CommSemiring.toSemiring ℝ Real.instCommSemiring)))) := inferInstanceend OAI.CKSInducedAreaendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSInducedAreaopen Bundle Manifold Set Bornology Filteropen scoped Bundle Manifold ContDiff Topologyvariable {H3 : Type*} [TopologicalSpace H3] {I3 : ModelWithCorners ℝ E3 H3} {N : Type*} [TopologicalSpace N] [ChartedSpace H3 N] [IsManifold I3 ∞ N] {S : Type u_3} [TopologicalSpace S] [ChartedSpace E2 S] [IsManifold I2 ∞ S]attribute [local instance] real_continuousAdd real_continuousConstSMul real_smulCommClass real_id_isometricabbrev Inner2 := letI := OAI.CKSInducedArea.real_smulCommClass ∀ x : S, TangentSpace OAI.CKSInducedArea.I2 x →L[ℝ] TangentSpace OAI.CKSInducedArea.I2 x →L[ℝ] ℝend OAI.CKSInducedAreaendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSInducedAreaopen Bundle Manifold Set Bornology Filteropen scoped Bundle Manifold ContDiff Topologyvariable {H3 : Type u_1} [TopologicalSpace H3] {I3 : ModelWithCorners ℝ E3 H3} {N : Type u_2} [TopologicalSpace N] [ChartedSpace H3 N] [IsManifold I3 ∞ N] {S : Type*} [TopologicalSpace S] [ChartedSpace E2 S] [IsManifold I2 ∞ S]attribute [local instance] real_continuousAdd real_continuousConstSMul real_smulCommClass real_id_isometricabbrev Smooth3 := ContMDiffRiemannianMetric I3 ∞ OAI.CKSInducedArea.E3 (fun x : N => TangentSpace I3 x)end OAI.CKSInducedAreaendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSInducedAreaopen Bundle Manifold Set Bornology Filteropen scoped Bundle Manifold ContDiff Topologyvariable {H3 : Type*} [TopologicalSpace H3] {I3 : ModelWithCorners ℝ E3 H3} {N : Type*} [TopologicalSpace N] [ChartedSpace H3 N] [IsManifold I3 ∞ N] {S : Type*} [TopologicalSpace S] [ChartedSpace E2 S] [IsManifold I2 ∞ S]attribute [local instance] real_continuousAdd real_continuousConstSMul real_smulCommClass real_id_isometricabbrev Bil2 := letI := OAI.CKSInducedArea.real_smulCommClass OAI.CKSInducedArea.E2 →L[ℝ] OAI.CKSInducedArea.E2 →L[ℝ] ℝabbrev Bil3 := letI := OAI.CKSInducedArea.real_smulCommClass OAI.CKSInducedArea.E3 →L[ℝ] OAI.CKSInducedArea.E3 →L[ℝ] ℝend OAI.CKSInducedAreaendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSInducedAreaopen Bundle Manifold Set Bornology Filteropen scoped Bundle Manifold ContDiff Topologyvariable {H3 : Type u_1} [TopologicalSpace H3] {I3 : ModelWithCorners ℝ E3 H3} {N : Type u_2} [TopologicalSpace N] [ChartedSpace H3 N] [IsManifold I3 ∞ N] {S : Type u_3} [TopologicalSpace S] [ChartedSpace E2 S] [IsManifold I2 ∞ S]attribute [local instance] real_continuousAdd real_continuousConstSMul real_smulCommClass real_id_isometricdef inducedInner (g : OAI.CKSInducedArea.Smooth3 (I3 := I3) (N := N)) (φ : S → N) : OAI.CKSInducedArea.Inner2 (S := S) := letI := OAI.CKSInducedArea.real_id_isometric letI := OAI.CKSInducedArea.real_id_compTriple fun x => by let : NormedAddCommGroup (TangentSpace OAI.CKSInducedArea.I2 x) := by unfold TangentSpace; infer_instance let : NormedSpace ℝ (TangentSpace OAI.CKSInducedArea.I2 x) := by unfold TangentSpace; infer_instance let : NormedAddCommGroup (TangentSpace I3 (φ x)) := by unfold TangentSpace; infer_instance let : NormedSpace ℝ (TangentSpace I3 (φ x)) := by unfold TangentSpace; infer_instance exact (g.inner (φ x)).bilinearComp (mfderiv OAI.CKSInducedArea.I2 I3 φ x) (mfderiv OAI.CKSInducedArea.I2 I3 φ x)end OAI.CKSInducedAreaendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSInducedAreaopen Bundle Manifold Set Bornology Filteropen scoped Bundle Manifold ContDiff Topologyvariable {H3 : Type*} [TopologicalSpace H3] {I3 : ModelWithCorners ℝ E3 H3} {N : Type*} [TopologicalSpace N] [ChartedSpace H3 N] [IsManifold I3 ∞ N] {S : Type*} [TopologicalSpace S] [ChartedSpace E2 S] [IsManifold I2 ∞ S]attribute [local instance] real_continuousAdd real_continuousConstSMul real_smulCommClass real_id_isometricvariable {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_5} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I ∞ M]local instance tangent_manifold_one : IsManifold I 1 M := inferInstanceend OAI.CKSInducedAreaendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSInducedAreaopen Bundle Manifold Set Bornology Filteropen scoped Bundle Manifold ContDiff Topologyvariable {H3 : Type*} [TopologicalSpace H3] {I3 : ModelWithCorners ℝ E3 H3} {N : Type*} [TopologicalSpace N] [ChartedSpace H3 N] [IsManifold I3 ∞ N] {S : Type*} [TopologicalSpace S] [ChartedSpace E2 S] [IsManifold I2 ∞ S]attribute [local instance] real_continuousAdd real_continuousConstSMul real_smulCommClass real_id_isometricvariable {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_5} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I ∞ M]attribute [local instance] tangent_manifold_onelocal instance tangent_vectorBundle : VectorBundle ℝ E (fun x : M => TangentSpace I x) := inferInstanceend OAI.CKSInducedAreaendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSInducedAreaopen Bundle Manifold Set Bornology Filteropen scoped Bundle Manifold ContDiff Topologyvariable {H3 : Type*} [TopologicalSpace H3] {I3 : ModelWithCorners ℝ E3 H3} {N : Type*} [TopologicalSpace N] [ChartedSpace H3 N] [IsManifold I3 ∞ N] {S : Type*} [TopologicalSpace S] [ChartedSpace E2 S] [IsManifold I2 ∞ S]attribute [local instance] real_continuousAdd real_continuousConstSMul real_smulCommClass real_id_isometricvariable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type*} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type*} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I ∞ M]attribute [local instance] tangent_manifold_oneattribute [local instance] tangent_vectorBundlelocal instance scalar_smulCommClass : SMulCommClass ℝ ℝ ℝ := inferInstanceend OAI.CKSInducedAreaendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSInducedAreaopen Bundle Manifold Set Bornology Filteropen scoped Bundle Manifold ContDiff Topologyvariable {H3 : Type*} [TopologicalSpace H3] {I3 : ModelWithCorners ℝ E3 H3} {N : Type*} [TopologicalSpace N] [ChartedSpace H3 N] [IsManifold I3 ∞ N] {S : Type*} [TopologicalSpace S] [ChartedSpace E2 S] [IsManifold I2 ∞ S]attribute [local instance] real_continuousAdd real_continuousConstSMul real_smulCommClass real_id_isometricvariable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type*} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I ∞ M]attribute [local instance] tangent_manifold_oneattribute [local instance] tangent_vectorBundleattribute [local instance] scalar_smulCommClasslocal instance scalar_vectorBundle : VectorBundle ℝ ℝ (Bundle.Trivial M ℝ) := inferInstanceend OAI.CKSInducedAreaendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSInducedAreaopen Bundle Manifold Set Bornology Filteropen scoped Bundle Manifold ContDiff Topologyvariable {H3 : Type*} [TopologicalSpace H3] {I3 : ModelWithCorners ℝ E3 H3} {N : Type*} [TopologicalSpace N] [ChartedSpace H3 N] [IsManifold I3 ∞ N] {S : Type*} [TopologicalSpace S] [ChartedSpace E2 S] [IsManifold I2 ∞ S]attribute [local instance] real_continuousAdd real_continuousConstSMul real_smulCommClass real_id_isometricvariable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type*} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type*} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I ∞ M]attribute [local instance] tangent_manifold_oneattribute [local instance] tangent_vectorBundleattribute [local instance] scalar_smulCommClassattribute [local instance] scalar_vectorBundlelocal instance scalar_continuousSMul : ContinuousSMul ℝ ℝ := inferInstanceend OAI.CKSInducedAreaendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSInducedAreaopen Bundle Manifold Set Bornology Filteropen scoped Bundle Manifold ContDiff Topologyvariable {H3 : Type*} [TopologicalSpace H3] {I3 : ModelWithCorners ℝ E3 H3} {N : Type*} [TopologicalSpace N] [ChartedSpace H3 N] [IsManifold I3 ∞ N] {S : Type*} [TopologicalSpace S] [ChartedSpace E2 S] [IsManifold I2 ∞ S]attribute [local instance] real_continuousAdd real_continuousConstSMul real_smulCommClass real_id_isometricvariable {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_5} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I ∞ M]attribute [local instance] tangent_manifold_oneattribute [local instance] tangent_vectorBundleattribute [local instance] scalar_smulCommClassattribute [local instance] scalar_vectorBundleattribute [local instance] scalar_continuousSMullocal instance covector_vectorBundle : VectorBundle ℝ (E →L[ℝ] ℝ) (fun x : M => TangentSpace I x →L[ℝ] ℝ) := inferInstanceend OAI.CKSInducedAreaendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSInducedAreaopen Bundle Manifold Set Bornology Filteropen scoped Bundle Manifold ContDiff Topologyvariable {H3 : Type*} [TopologicalSpace H3] {I3 : ModelWithCorners ℝ E3 H3} {N : Type*} [TopologicalSpace N] [ChartedSpace H3 N] [IsManifold I3 ∞ N] {S : Type*} [TopologicalSpace S] [ChartedSpace E2 S] [IsManifold I2 ∞ S]attribute [local instance] real_continuousAdd real_continuousConstSMul real_smulCommClass real_id_isometricvariable {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_5} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I ∞ M]attribute [local instance] tangent_manifold_oneattribute [local instance] tangent_vectorBundleattribute [local instance] scalar_smulCommClassattribute [local instance] scalar_vectorBundleattribute [local instance] scalar_continuousSMulattribute [local instance] covector_vectorBundlelocal instance covector_topologicalAddGroup (x : M) : IsTopologicalAddGroup (TangentSpace I x →L[ℝ] ℝ) := inferInstanceend OAI.CKSInducedAreaendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSInducedAreaopen Bundle Manifold Set Bornology Filteropen scoped Bundle Manifold ContDiff Topologyvariable {H3 : Type*} [TopologicalSpace H3] {I3 : ModelWithCorners ℝ E3 H3} {N : Type*} [TopologicalSpace N] [ChartedSpace H3 N] [IsManifold I3 ∞ N] {S : Type*} [TopologicalSpace S] [ChartedSpace E2 S] [IsManifold I2 ∞ S]attribute [local instance] real_continuousAdd real_continuousConstSMul real_smulCommClass real_id_isometricvariable {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_5} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I ∞ M]attribute [local instance] tangent_manifold_oneattribute [local instance] tangent_vectorBundleattribute [local instance] scalar_smulCommClassattribute [local instance] scalar_vectorBundleattribute [local instance] scalar_continuousSMulattribute [local instance] covector_vectorBundleattribute [local instance] covector_topologicalAddGrouplocal instance covector_continuousSMul (x : M) : ContinuousSMul ℝ (TangentSpace I x →L[ℝ] ℝ) := inferInstanceend OAI.CKSInducedAreaendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSInducedAreaopen Bundle Manifold Set Bornology Filteropen scoped Bundle Manifold ContDiff Topologyvariable {H3 : Type*} [TopologicalSpace H3] {I3 : ModelWithCorners ℝ E3 H3} {N : Type*} [TopologicalSpace N] [ChartedSpace H3 N] [IsManifold I3 ∞ N] {S : Type*} [TopologicalSpace S] [ChartedSpace E2 S] [IsManifold I2 ∞ S]attribute [local instance] real_continuousAdd real_continuousConstSMul real_smulCommClass real_id_isometricvariable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type*} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I ∞ M]attribute [local instance] tangent_manifold_oneattribute [local instance] tangent_vectorBundleattribute [local instance] scalar_smulCommClassattribute [local instance] scalar_vectorBundleattribute [local instance] scalar_continuousSMulattribute [local instance] covector_vectorBundleattribute [local instance] covector_topologicalAddGroupattribute [local instance] covector_continuousSMullocal instance scalarAtlas : MemTrivializationAtlas (Bundle.Trivial.trivialization M ℝ) := ⟨rfl⟩end OAI.CKSInducedAreaendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSInducedAreaopen Bundle Manifold Set Bornology Filteropen scoped Bundle Manifold ContDiff Topologyvariable {H3 : Type*} [TopologicalSpace H3] {I3 : ModelWithCorners ℝ E3 H3} {N : Type*} [TopologicalSpace N] [ChartedSpace H3 N] [IsManifold I3 ∞ N] {S : Type*} [TopologicalSpace S] [ChartedSpace E2 S] [IsManifold I2 ∞ S]attribute [local instance] real_continuousAdd real_continuousConstSMul real_smulCommClass real_id_isometricvariable {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_5} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I ∞ M]attribute [local instance] tangent_manifold_oneattribute [local instance] tangent_vectorBundleattribute [local instance] scalar_smulCommClassattribute [local instance] scalar_vectorBundleattribute [local instance] scalar_continuousSMulattribute [local instance] covector_vectorBundleattribute [local instance] covector_topologicalAddGroupattribute [local instance] covector_continuousSMulattribute [local instance] OAI.CKSInducedArea.scalarAtlaslocal instance covector_atlas (e : Trivialization E (π E (fun x : M => TangentSpace I x))) [MemTrivializationAtlas e] : MemTrivializationAtlas (e.continuousLinearMap (RingHom.id ℝ) (Bundle.Trivial.trivialization M ℝ)) := inferInstanceend OAI.CKSInducedAreaendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSInducedAreaopen Bundle Manifold Set Bornology Filteropen scoped Bundle Manifold ContDiff Topologyvariable {H3 : Type*} [TopologicalSpace H3] {I3 : ModelWithCorners ℝ E3 H3} {N : Type*} [TopologicalSpace N] [ChartedSpace H3 N] [IsManifold I3 ∞ N] {S : Type*} [TopologicalSpace S] [ChartedSpace E2 S] [IsManifold I2 ∞ S]attribute [local instance] real_continuousAdd real_continuousConstSMul real_smulCommClass real_id_isometricvariable {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_5} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I ∞ M]attribute [local instance] tangent_manifold_oneattribute [local instance] tangent_vectorBundleattribute [local instance] scalar_smulCommClassattribute [local instance] scalar_vectorBundleattribute [local instance] scalar_continuousSMulattribute [local instance] covector_vectorBundleattribute [local instance] covector_topologicalAddGroupattribute [local instance] covector_continuousSMulattribute [local instance] OAI.CKSInducedArea.scalarAtlasattribute [local instance] covector_atlasdef bilinearTriv (e : Trivialization E (π E (fun x : M => TangentSpace I x))) [MemTrivializationAtlas e] : Trivialization (E →L[ℝ] E →L[ℝ] ℝ) (π (E →L[ℝ] E →L[ℝ] ℝ) (fun x : M => TangentSpace I x →L[ℝ] TangentSpace I x →L[ℝ] ℝ)) := letI := OAI.CKSInducedArea.real_smulCommClass e.continuousLinearMap (RingHom.id ℝ) (e.continuousLinearMap (RingHom.id ℝ) (Bundle.Trivial.trivialization M ℝ))instance bilinearTriv_atlas (e : Trivialization E (π E (fun x : M => TangentSpace I x))) [MemTrivializationAtlas e] : MemTrivializationAtlas (OAI.CKSInducedArea.bilinearTriv I e) := by unfold OAI.CKSInducedArea.bilinearTriv infer_instanceend OAI.CKSInducedAreaendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSInducedAreaopen Bundle Manifold Set Bornology Filteropen scoped Bundle Manifold ContDiff Topologyvariable {H3 : Type*} [TopologicalSpace H3] {I3 : ModelWithCorners ℝ E3 H3} {N : Type*} [TopologicalSpace N] [ChartedSpace H3 N] [IsManifold I3 ∞ N] {S : Type*} [TopologicalSpace S] [ChartedSpace E2 S] [IsManifold I2 ∞ S]attribute [local instance] real_continuousAdd real_continuousConstSMul real_smulCommClass real_id_isometriclocal instance covector_smulCommClass {Space : Type u_4} [NormedAddCommGroup Space] [NormedSpace ℝ Space] : letI := OAI.CKSInducedArea.real_smulCommClass SMulCommClass ℝ ℝ (Space →L[ℝ] ℝ) := by infer_instancelocal instance bilNorm2 : NormedAddCommGroup OAI.CKSInducedArea.Bil2 := letI := OAI.CKSInducedArea.real_smulCommClass ContinuousLinearMap.toNormedAddCommGroup (E := OAI.CKSInducedArea.E2) (F := OAI.CKSInducedArea.E2 →L[ℝ] ℝ) (σ₁₂ := RingHom.id ℝ)end OAI.CKSInducedAreaendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSInducedAreaopen Bundle Manifold Set Bornology Filteropen scoped Bundle Manifold ContDiff Topologyvariable {H3 : Type*} [TopologicalSpace H3] {I3 : ModelWithCorners ℝ E3 H3} {N : Type*} [TopologicalSpace N] [ChartedSpace H3 N] [IsManifold I3 ∞ N] {S : Type*} [TopologicalSpace S] [ChartedSpace E2 S] [IsManifold I2 ∞ S]attribute [local instance] real_continuousAdd real_continuousConstSMul real_smulCommClass real_id_isometricattribute [local instance] OAI.CKSInducedArea.bilNorm2local instance bilSpace2 : NormedSpace ℝ OAI.CKSInducedArea.Bil2 := letI := OAI.CKSInducedArea.real_smulCommClass letI := OAI.CKSInducedArea.covector_smulCommClass (Space := OAI.CKSInducedArea.E2) ContinuousLinearMap.toNormedSpaceend OAI.CKSInducedAreaendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSInducedAreaopen Bundle Manifold Set Bornology Filteropen scoped Bundle Manifold ContDiff Topologyvariable {H3 : Type*} [TopologicalSpace H3] {I3 : ModelWithCorners ℝ E3 H3} {N : Type*} [TopologicalSpace N] [ChartedSpace H3 N] [IsManifold I3 ∞ N] {S : Type*} [TopologicalSpace S] [ChartedSpace E2 S] [IsManifold I2 ∞ S]attribute [local instance] real_continuousAdd real_continuousConstSMul real_smulCommClass real_id_isometricattribute [local instance] OAI.CKSInducedArea.bilNorm2attribute [local instance] OAI.CKSInducedArea.bilSpace2local instance bilNorm3 : NormedAddCommGroup OAI.CKSInducedArea.Bil3 := letI := OAI.CKSInducedArea.real_smulCommClass ContinuousLinearMap.toNormedAddCommGroup (E := OAI.CKSInducedArea.E3) (F := OAI.CKSInducedArea.E3 →L[ℝ] ℝ) (σ₁₂ := RingHom.id ℝ)end OAI.CKSInducedAreaendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSInducedAreaopen Bundle Manifold Set Bornology Filteropen scoped Bundle Manifold ContDiff Topologyvariable {H3 : Type*} [TopologicalSpace H3] {I3 : ModelWithCorners ℝ E3 H3} {N : Type*} [TopologicalSpace N] [ChartedSpace H3 N] [IsManifold I3 ∞ N] {S : Type*} [TopologicalSpace S] [ChartedSpace E2 S] [IsManifold I2 ∞ S]attribute [local instance] real_continuousAdd real_continuousConstSMul real_smulCommClass real_id_isometricattribute [local instance] OAI.CKSInducedArea.bilNorm2attribute [local instance] OAI.CKSInducedArea.bilSpace2attribute [local instance] OAI.CKSInducedArea.bilNorm3local instance bilSpace3 : NormedSpace ℝ OAI.CKSInducedArea.Bil3 := letI := OAI.CKSInducedArea.real_smulCommClass letI := OAI.CKSInducedArea.covector_smulCommClass (Space := OAI.CKSInducedArea.E3) ContinuousLinearMap.toNormedSpaceend OAI.CKSInducedAreaendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSInducedAreaopen Bundle Manifold Set Bornology Filteropen scoped Bundle Manifold ContDiff Topologyvariable {H3 : Type*} [TopologicalSpace H3] {I3 : ModelWithCorners ℝ E3 H3} {N : Type*} [TopologicalSpace N] [ChartedSpace H3 N] [IsManifold I3 ∞ N] {S : Type*} [TopologicalSpace S] [ChartedSpace E2 S] [IsManifold I2 ∞ S]attribute [local instance] real_continuousAdd real_continuousConstSMul real_smulCommClass real_id_isometricattribute [local instance] OAI.CKSInducedArea.bilNorm2attribute [local instance] OAI.CKSInducedArea.bilSpace2attribute [local instance] OAI.CKSInducedArea.bilNorm3attribute [local instance] OAI.CKSInducedArea.bilSpace3local instance mixNorm23 : NormedAddCommGroup (OAI.CKSInducedArea.E2 →L[ℝ] OAI.CKSInducedArea.E3 →L[ℝ] ℝ) := letI := OAI.CKSInducedArea.real_smulCommClass ContinuousLinearMap.toNormedAddCommGroup (E := OAI.CKSInducedArea.E2) (F := OAI.CKSInducedArea.E3 →L[ℝ] ℝ) (σ₁₂ := RingHom.id ℝ)end OAI.CKSInducedAreaendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSInducedAreaopen Bundle Manifold Set Bornology Filteropen scoped Bundle Manifold ContDiff Topologyvariable {H3 : Type*} [TopologicalSpace H3] {I3 : ModelWithCorners ℝ E3 H3} {N : Type*} [TopologicalSpace N] [ChartedSpace H3 N] [IsManifold I3 ∞ N] {S : Type*} [TopologicalSpace S] [ChartedSpace E2 S] [IsManifold I2 ∞ S]attribute [local instance] real_continuousAdd real_continuousConstSMul real_smulCommClass real_id_isometricattribute [local instance] OAI.CKSInducedArea.bilNorm2attribute [local instance] OAI.CKSInducedArea.bilSpace2attribute [local instance] OAI.CKSInducedArea.bilNorm3attribute [local instance] OAI.CKSInducedArea.bilSpace3attribute [local instance] OAI.CKSInducedArea.mixNorm23local instance mixSpace23 : NormedSpace ℝ (OAI.CKSInducedArea.E2 →L[ℝ] OAI.CKSInducedArea.E3 →L[ℝ] ℝ) := letI := OAI.CKSInducedArea.real_smulCommClass letI := OAI.CKSInducedArea.covector_smulCommClass (Space := OAI.CKSInducedArea.E3) ContinuousLinearMap.toNormedSpaceend OAI.CKSInducedAreaendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSInducedAreaopen Bundle Manifold Set Bornology Filteropen scoped Bundle Manifold ContDiff Topologyvariable {H3 : Type*} [TopologicalSpace H3] {I3 : ModelWithCorners ℝ E3 H3} {N : Type*} [TopologicalSpace N] [ChartedSpace H3 N] [IsManifold I3 ∞ N] {S : Type*} [TopologicalSpace S] [ChartedSpace E2 S] [IsManifold I2 ∞ S]attribute [local instance] real_continuousAdd real_continuousConstSMul real_smulCommClass real_id_isometricattribute [local instance] OAI.CKSInducedArea.bilNorm2attribute [local instance] OAI.CKSInducedArea.bilSpace2attribute [local instance] OAI.CKSInducedArea.bilNorm3attribute [local instance] OAI.CKSInducedArea.bilSpace3attribute [local instance] OAI.CKSInducedArea.mixNorm23attribute [local instance] OAI.CKSInducedArea.mixSpace23local instance mixNorm32 : NormedAddCommGroup (OAI.CKSInducedArea.E3 →L[ℝ] OAI.CKSInducedArea.E2 →L[ℝ] ℝ) := letI := OAI.CKSInducedArea.real_smulCommClass ContinuousLinearMap.toNormedAddCommGroup (E := OAI.CKSInducedArea.E3) (F := OAI.CKSInducedArea.E2 →L[ℝ] ℝ) (σ₁₂ := RingHom.id ℝ)end OAI.CKSInducedAreaendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSInducedAreaopen Bundle Manifold Set Bornology Filteropen scoped Bundle Manifold ContDiff Topologyvariable {H3 : Type*} [TopologicalSpace H3] {I3 : ModelWithCorners ℝ E3 H3} {N : Type*} [TopologicalSpace N] [ChartedSpace H3 N] [IsManifold I3 ∞ N] {S : Type*} [TopologicalSpace S] [ChartedSpace E2 S] [IsManifold I2 ∞ S]attribute [local instance] real_continuousAdd real_continuousConstSMul real_smulCommClass real_id_isometricattribute [local instance] OAI.CKSInducedArea.bilNorm2attribute [local instance] OAI.CKSInducedArea.bilSpace2attribute [local instance] OAI.CKSInducedArea.bilNorm3attribute [local instance] OAI.CKSInducedArea.bilSpace3attribute [local instance] OAI.CKSInducedArea.mixNorm23attribute [local instance] OAI.CKSInducedArea.mixSpace23attribute [local instance] OAI.CKSInducedArea.mixNorm32local instance mixSpace32 : NormedSpace ℝ (OAI.CKSInducedArea.E3 →L[ℝ] OAI.CKSInducedArea.E2 →L[ℝ] ℝ) := letI := OAI.CKSInducedArea.real_smulCommClass letI := OAI.CKSInducedArea.covector_smulCommClass (Space := OAI.CKSInducedArea.E2) ContinuousLinearMap.toNormedSpaceend OAI.CKSInducedAreaendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSInducedAreaopen Bundle Manifold Set Bornology Filteropen scoped Bundle Manifold ContDiff Topologyvariable {H3 : Type u_1} [TopologicalSpace H3] {I3 : ModelWithCorners ℝ E3 H3} {N : Type u_2} [TopologicalSpace N] [ChartedSpace H3 N] [IsManifold I3 ∞ N] {S : Type u_3} [TopologicalSpace S] [ChartedSpace E2 S] [IsManifold I2 ∞ S]attribute [local instance] real_continuousAdd real_continuousConstSMul real_smulCommClass real_id_isometricattribute [local instance] OAI.CKSInducedArea.bilNorm2attribute [local instance] OAI.CKSInducedArea.bilSpace2attribute [local instance] OAI.CKSInducedArea.bilNorm3attribute [local instance] OAI.CKSInducedArea.bilSpace3attribute [local instance] OAI.CKSInducedArea.mixNorm23attribute [local instance] OAI.CKSInducedArea.mixSpace23attribute [local instance] OAI.CKSInducedArea.mixNorm32attribute [local instance] OAI.CKSInducedArea.mixSpace32def inducedMetric (g : OAI.CKSInducedArea.Smooth3 (I3 := I3) (N := N)) (φ : S → N) (hφ : ContMDiff OAI.CKSInducedArea.I2 I3 ∞ φ) (hinj : ∀ x, Function.Injective (mfderiv OAI.CKSInducedArea.I2 I3 φ x)) : ContMDiffRiemannianMetric OAI.CKSInducedArea.I2 ∞ OAI.CKSInducedArea.E2 (fun x : S => TangentSpace OAI.CKSInducedArea.I2 x) := have proof_inducedInner_symm_37 {H3 : Type u_1} [instLocal1 : TopologicalSpace.{u_1} H3] {I3 : ModelWithCorners.{0, 0, u_1} ℝ OAI.CKSInducedArea.E3 H3} {N : Type u_2} [instLocal4 : TopologicalSpace.{u_2} N] [instLocal5 : ChartedSpace.{u_1, u_2} H3 N] [instLocal6 : IsManifold.{0, 0, u_1, u_2} I3 (∞ : ℕ∞ω) N] {S : Type u_3} [instLocal8 : TopologicalSpace.{u_3} S] [instLocal9 : ChartedSpace.{0, u_3} OAI.CKSInducedArea.E2 S] (metric : OAI.CKSInducedArea.Smooth3 (I3 := I3) (N := N)) (immersion : S → N) (point : S) (left right : TangentSpace OAI.CKSInducedArea.I2 point) : OAI.CKSInducedArea.inducedInner metric immersion point left right = OAI.CKSInducedArea.inducedInner metric immersion point right left := metric.symm (immersion point) _ _ have proof_inducedInner_pos_38 {H3 : Type u_1} [instLocal1 : TopologicalSpace.{u_1} H3] {I3 : ModelWithCorners.{0, 0, u_1} ℝ OAI.CKSInducedArea.E3 H3} {N : Type u_2} [instLocal4 : TopologicalSpace.{u_2} N] [instLocal5 : ChartedSpace.{u_1, u_2} H3 N] [instLocal6 : IsManifold.{0, 0, u_1, u_2} I3 (∞ : ℕ∞ω) N] {S : Type u_3} [instLocal8 : TopologicalSpace.{u_3} S] [instLocal9 : ChartedSpace.{0, u_3} OAI.CKSInducedArea.E2 S] (metric : OAI.CKSInducedArea.Smooth3 (I3 := I3) (N := N)) (immersion : S → N) (injective : ∀ point, Function.Injective (mfderiv OAI.CKSInducedArea.I2 I3 immersion point)) (point : S) (vector : TangentSpace OAI.CKSInducedArea.I2 point) (nonzero : vector ≠ 0) : 0 < OAI.CKSInducedArea.inducedInner metric immersion point vector vector := metric.pos (immersion point) _ (fun zero => nonzero (injective point (zero.trans (map_zero _).symm))) have proof_positive_bilinear_bounded_41 (B : OAI.CKSInducedArea.Bil2) (hB : ∀ v : OAI.CKSInducedArea.E2, v ≠ 0 → 0 < B v v) : IsVonNBounded ℝ {v : OAI.CKSInducedArea.E2 | B v v < 1} := by have hc : Continuous (fun v : OAI.CKSInducedArea.E2 => B v v) := B.continuous.clm_apply continuous_id obtain ⟨a,ha,hm⟩ := (isCompact_sphere (0 : OAI.CKSInducedArea.E2) 1).exists_isMinOn (NormedSpace.sphere_nonempty.mpr (by norm_num : (0 : ℝ) ≤ 1)) hc.continuousOn have haNorm : ‖a‖ = 1 := by simpa [Metric.mem_sphere] using ha have ha0 : a ≠ 0 := by intro h; simp [h] at haNorm have hp : 0 < B a a := hB a ha0 have hlow : ∀ v : OAI.CKSInducedArea.E2, B a a * ‖v‖ ^ 2 ≤ B v v := by intro v by_cases hv : v = 0 · simp [hv] have hn : 0 < ‖v‖ := norm_pos_iff.mpr hv have hy : ‖(‖v‖⁻¹ : ℝ) • v‖ = 1 := by rw [norm_smul, Real.norm_eq_abs, abs_of_pos (inv_pos.mpr hn), inv_mul_cancel₀ hn.ne'] have h := hm (show (‖v‖⁻¹ : ℝ) • v ∈ Metric.sphere (0 : OAI.CKSInducedArea.E2) 1 by simpa [Metric.mem_sphere] using hy) have he : B ((‖v‖⁻¹ : ℝ) • v) ((‖v‖⁻¹ : ℝ) • v) = B v v / ‖v‖^2 := by simp only [map_smul, smul_apply, smul_eq_mul] field_simp change B a a ≤ B ((‖v‖⁻¹ : ℝ) • v) ((‖v‖⁻¹ : ℝ) • v) at h rw [he] at h exact (le_div_iff₀ (sq_pos_of_pos hn)).mp h apply (NormedSpace.isVonNBounded_iff ℝ).mpr apply (Metric.isBounded_iff_subset_ball (0 : OAI.CKSInducedArea.E2)).mpr refine ⟨1 + (B a a)⁻¹, ?_⟩ intro v hv change dist v 0 < 1 + (B a a)⁻¹ rw [dist_zero_right] have hbv : B v v < 1 := hv have hl := hlow v have hinv : 0 < (B a a)⁻¹ := inv_pos.mpr hp have he : B a a * (B a a)⁻¹ = 1 := mul_inv_cancel₀ hp.ne' by_contra hh have hn : 1 + (B a a)⁻¹ ≤ ‖v‖ := le_of_not_gt hh have hn1 : 1 ≤ ‖v‖ := by linarith have hn2 : ‖v‖ ≤ ‖v‖^2 := by nlinarith have hmul := mul_le_mul_of_nonneg_left hn hp.le have hmul2 := mul_le_mul_of_nonneg_left hn2 hp.le nlinarith have proof_inducedInner_bounded_39 {H3 : Type u_1} [instLocal1 : TopologicalSpace.{u_1} H3] {I3 : ModelWithCorners.{0, 0, u_1} ℝ OAI.CKSInducedArea.E3 H3} {N : Type u_2} [instLocal4 : TopologicalSpace.{u_2} N] [instLocal5 : ChartedSpace.{u_1, u_2} H3 N] [instLocal6 : IsManifold.{0, 0, u_1, u_2} I3 (∞ : ℕ∞ω) N] {S : Type u_3} [instLocal8 : TopologicalSpace.{u_3} S] [instLocal9 : ChartedSpace.{0, u_3} OAI.CKSInducedArea.E2 S] (metric : OAI.CKSInducedArea.Smooth3 (I3 := I3) (N := N)) (immersion : S → N) (injective : ∀ point, Function.Injective (mfderiv OAI.CKSInducedArea.I2 I3 immersion point)) (point : S) : IsVonNBounded ℝ {vector : TangentSpace OAI.CKSInducedArea.I2 point | inducedInner metric immersion point vector vector < 1} := proof_positive_bilinear_bounded_41 (OAI.CKSInducedArea.inducedInner metric immersion point) (proof_inducedInner_pos_38 metric immersion injective point) have proof_bilinearComp_smoothAt_42 {S : Type u_3} [instLocal1 : TopologicalSpace.{u_3} S] [instLocal2 : ChartedSpace.{0, u_3} OAI.CKSInducedArea.E2 S] [instLocal3 : IsManifold.{0, 0, 0, u_3} OAI.CKSInducedArea.I2 (∞ : ℕ∞ω) S] [IsManifold OAI.CKSInducedArea.I2 ∞ S] {B : S → OAI.CKSInducedArea.Bil3} {A : S → OAI.CKSInducedArea.E2 →L[ℝ] OAI.CKSInducedArea.E3} {x : S} (hB : ContMDiffAt OAI.CKSInducedArea.I2 𝓘(ℝ,OAI.CKSInducedArea.Bil3) ∞ B x) (hA : ContMDiffAt OAI.CKSInducedArea.I2 𝓘(ℝ,OAI.CKSInducedArea.E2 →L[ℝ] OAI.CKSInducedArea.E3) ∞ A x) : ContMDiffAt OAI.CKSInducedArea.I2 𝓘(ℝ,OAI.CKSInducedArea.Bil2) ∞ (fun y => (B y).bilinearComp (A y) (A y)) x := by have flip1 : ContDiff ℝ ∞ (fun B : OAI.CKSInducedArea.E2 →L[ℝ] OAI.CKSInducedArea.E3 →L[ℝ] ℝ => B.flip) := by let L : (OAI.CKSInducedArea.E2 →L[ℝ] OAI.CKSInducedArea.E3 →L[ℝ] ℝ) →L[ℝ] (OAI.CKSInducedArea.E3 →L[ℝ] OAI.CKSInducedArea.E2 →L[ℝ] ℝ) := (ContinuousLinearMap.flipₗᵢ ℝ OAI.CKSInducedArea.E2 OAI.CKSInducedArea.E3 ℝ).toContinuousLinearEquiv.toContinuousLinearMap exact L.contDiff have flip2 : ContDiff ℝ ∞ (fun B : OAI.CKSInducedArea.Bil2 => B.flip) := by let L : OAI.CKSInducedArea.Bil2 →L[ℝ] OAI.CKSInducedArea.Bil2 := (ContinuousLinearMap.flipₗᵢ ℝ OAI.CKSInducedArea.E2 OAI.CKSInducedArea.E2 ℝ).toContinuousLinearEquiv.toContinuousLinearMap exact L.contDiff exact flip2.comp_contMDiffAt ((flip1.comp_contMDiffAt (hB.clm_comp hA)).clm_comp hA) have proof_bilinearTriv_pair_43 {E : Type 0} [instLocal1 : NormedAddCommGroup.{0} E] [instLocal2 : NormedSpace.{0, 0} ℝ E] {H : Type 0} [instLocal4 : TopologicalSpace.{0} H] (I : ModelWithCorners.{0, 0, 0} ℝ E H) {M : Type u_3} [instLocal7 : TopologicalSpace.{u_3} M] [instLocal8 : ChartedSpace.{0, u_3} H M] [instLocal9 : IsManifold.{0, 0, 0, u_3} I (∞ : ℕ∞ω) M] (e : Trivialization E (π E (fun x : M => TangentSpace I x))) [MemTrivializationAtlas e] {x : M} (hx : x ∈ e.baseSet) (B : TangentSpace I x →L[ℝ] TangentSpace I x →L[ℝ] ℝ) (v w : E) : ((OAI.CKSInducedArea.bilinearTriv I e) ⟨x,B⟩).2 v w = B (e.symmL ℝ x v) (e.symmL ℝ x w) := by let := OAI.CKSInducedArea.scalarAtlas (M := M) unfold OAI.CKSInducedArea.bilinearTriv rw [Trivialization.continuousLinearMap_apply] dsimp only [ContinuousLinearMap.comp_apply] rw [Trivialization.continuousLinearMapAt_apply_of_mem (R := ℝ) (e.continuousLinearMap (RingHom.id ℝ) (Trivial.trivialization M ℝ)) (show x ∈ (e.continuousLinearMap (RingHom.id ℝ) (Trivial.trivialization M ℝ)).baseSet by simpa using hx)] rw [Trivialization.continuousLinearMap_apply] dsimp only [ContinuousLinearMap.comp_apply] rw [Trivialization.continuousLinearMapAt_apply_of_mem (R := ℝ) (Trivial.trivialization M ℝ) (show x ∈ (Trivial.trivialization M ℝ).baseSet from mem_univ x)] rfl have proof_bilinearTriv_pair_44 {E : Type 0} [instLocal1 : NormedAddCommGroup.{0} E] [instLocal2 : NormedSpace.{0, 0} ℝ E] {H : Type u_1} [instLocal4 : TopologicalSpace.{u_1} H] (I : ModelWithCorners.{0, 0, u_1} ℝ E H) {M : Type u_2} [instLocal7 : TopologicalSpace.{u_2} M] [instLocal8 : ChartedSpace.{u_1, u_2} H M] [instLocal9 : IsManifold.{0, 0, u_1, u_2} I (∞ : ℕ∞ω) M] (e : Trivialization E (π E (fun x : M => TangentSpace I x))) [MemTrivializationAtlas e] {x : M} (hx : x ∈ e.baseSet) (B : TangentSpace I x →L[ℝ] TangentSpace I x →L[ℝ] ℝ) (v w : E) : ((OAI.CKSInducedArea.bilinearTriv I e) ⟨x,B⟩).2 v w = B (e.symmL ℝ x v) (e.symmL ℝ x w) := by let := OAI.CKSInducedArea.scalarAtlas (M := M) unfold OAI.CKSInducedArea.bilinearTriv rw [Trivialization.continuousLinearMap_apply] dsimp only [ContinuousLinearMap.comp_apply] rw [Trivialization.continuousLinearMapAt_apply_of_mem (R := ℝ) (e.continuousLinearMap (RingHom.id ℝ) (Trivial.trivialization M ℝ)) (show x ∈ (e.continuousLinearMap (RingHom.id ℝ) (Trivial.trivialization M ℝ)).baseSet by simpa using hx)] rw [Trivialization.continuousLinearMap_apply] dsimp only [ContinuousLinearMap.comp_apply] rw [Trivialization.continuousLinearMapAt_apply_of_mem (R := ℝ) (Trivial.trivialization M ℝ) (show x ∈ (Trivial.trivialization M ℝ).baseSet from mem_univ x)] rfl have proof_inducedInner_smooth_40 {H3 : Type u_1} [instLocal1 : TopologicalSpace.{u_1} H3] {I3 : ModelWithCorners.{0, 0, u_1} ℝ OAI.CKSInducedArea.E3 H3} {N : Type u_2} [instLocal4 : TopologicalSpace.{u_2} N] [instLocal5 : ChartedSpace.{u_1, u_2} H3 N] [instLocal6 : IsManifold.{0, 0, u_1, u_2} I3 (∞ : ℕ∞ω) N] {S : Type u_3} [instLocal8 : TopologicalSpace.{u_3} S] [instLocal9 : ChartedSpace.{0, u_3} OAI.CKSInducedArea.E2 S] [instLocal10 : IsManifold.{0, 0, 0, u_3} OAI.CKSInducedArea.I2 (∞ : ℕ∞ω) S] (g : OAI.CKSInducedArea.Smooth3 (I3 := I3) (N := N)) {φ : S → N} (hφ : ContMDiff OAI.CKSInducedArea.I2 I3 ∞ φ) : ContMDiff OAI.CKSInducedArea.I2 (OAI.CKSInducedArea.I2.prod 𝓘(ℝ,OAI.CKSInducedArea.Bil2)) ∞ (fun x => TotalSpace.mk' OAI.CKSInducedArea.Bil2 x (OAI.CKSInducedArea.inducedInner g φ x)) := by let := OAI.CKSInducedArea.real_id_isometric let := OAI.CKSInducedArea.real_smulCommClass intro x let e := trivializationAt OAI.CKSInducedArea.E2 (TangentSpace OAI.CKSInducedArea.I2) x let e' := trivializationAt OAI.CKSInducedArea.E3 (TangentSpace I3) (φ x) have hx : x ∈ e.baseSet := mem_baseSet_trivializationAt OAI.CKSInducedArea.E2 (TangentSpace OAI.CKSInducedArea.I2) x have hx' : φ x ∈ e'.baseSet := mem_baseSet_trivializationAt OAI.CKSInducedArea.E3 (TangentSpace I3) (φ x) apply (contMDiffAt_section (𝕜 := ℝ) (B := S) (E := fun z : S => TangentSpace OAI.CKSInducedArea.I2 z →L[ℝ] TangentSpace OAI.CKSInducedArea.I2 z →L[ℝ] ℝ) (IB := OAI.CKSInducedArea.I2) (n := ∞) (F := OAI.CKSInducedArea.Bil2) (s := OAI.CKSInducedArea.inducedInner g φ) x).mpr change ContMDiffAt OAI.CKSInducedArea.I2 𝓘(ℝ,OAI.CKSInducedArea.Bil2) ∞ (fun y : S => ((OAI.CKSInducedArea.bilinearTriv OAI.CKSInducedArea.I2 e) ⟨y, OAI.CKSInducedArea.inducedInner g φ y⟩).2) x have hB := (contMDiffAt_section (𝕜 := ℝ) (B := N) (E := fun z : N => TangentSpace I3 z →L[ℝ] TangentSpace I3 z →L[ℝ] ℝ) (IB := I3) (n := ∞) (F := OAI.CKSInducedArea.Bil3) (s := g.inner) (φ x)).mp (g.contMDiff (φ x)) change ContMDiffAt I3 𝓘(ℝ,OAI.CKSInducedArea.Bil3) ∞ (fun y : N => ((OAI.CKSInducedArea.bilinearTriv I3 e') ⟨y, g.inner y⟩).2) (φ x) at hB have hD := (hφ x).mfderiv_const (show (∞ : ℕ∞ω) + 1 ≤ ∞ by simp [*]) apply (proof_bilinearComp_smoothAt_42 (hB.comp x (hφ x)) hD).congr_of_eventuallyEq filter_upwards [e.open_baseSet.mem_nhds hx, hφ.continuous.continuousAt.preimage_mem_nhds (e'.open_baseSet.mem_nhds hx')] with y hy hy' ext v w rw [proof_bilinearTriv_pair_43 OAI.CKSInducedArea.I2 e hy] rw [ContinuousLinearMap.bilinearComp_apply] dsimp only [Function.comp_apply] rw [proof_bilinearTriv_pair_44 I3 e' hy'] dsimp [OAI.CKSInducedArea.inducedInner,inTangentCoordinates,ContinuousLinearMap.inCoordinates] rw [e'.symmL_continuousLinearMapAt hy', e'.symmL_continuousLinearMapAt hy'] rfl { inner := OAI.CKSInducedArea.inducedInner g φ symm := proof_inducedInner_symm_37 g φ pos := proof_inducedInner_pos_38 g φ hinj isVonNBounded := proof_inducedInner_bounded_39 g φ hinj contMDiff := proof_inducedInner_smooth_40 g hφ }end OAI.CKSInducedAreaendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSEmbeddingDerivativeopen Set Manifold Bundle Filter Functionopen scoped ContDiff Topologyabbrev E := EuclideanSpace ℝ (Fin 3)local instance halfSpaceDimension_neZero : NeZero (3 : ℕ) := inferInstanceabbrev H := @EuclideanHalfSpace 3 OAI.CKSEmbeddingDerivative.halfSpaceDimension_neZeroabbrev I := @modelWithCornersEuclideanHalfSpace 3 OAI.CKSEmbeddingDerivative.halfSpaceDimension_neZeroend OAI.CKSEmbeddingDerivativeendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSFullCutAreaopen Set Manifold Bundle Functionopen scoped ContDiff Topologyopen CKSGeometricCuts (OuterDomain)open CKSBoundarySurfacevariable {N : Type u} [TopologicalSpace N] [ChartedSpace H3 N]instance domainTopology (D : OAI.CKSGeometricCuts.OuterDomain N) : TopologicalSpace D.Carrier := D.topologyinstance domainCharts (D : OAI.CKSGeometricCuts.OuterDomain N) : ChartedSpace OAI.CKSBoundarySurface.H3 D.Carrier := D.chartsinstance domainSmooth (D : OAI.CKSGeometricCuts.OuterDomain N) : IsManifold OAI.CKSBoundarySurface.I3 ∞ D.Carrier := D.smoothabbrev Surface (D : OAI.CKSGeometricCuts.OuterDomain N) := OAI.CKSBoundarySurface.Boundary D.Carrierdef cutInclusion (D : OAI.CKSGeometricCuts.OuterDomain N) : OAI.CKSFullCutArea.Surface D → N := D.inclusion ∘ Subtype.valend OAI.CKSFullCutAreaendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSFullCutAreaopen Set Manifold Bundle Functionopen scoped ContDiff Topologyopen CKSGeometricCuts (OuterDomain)open CKSBoundarySurfacevariable {N : Type u} [TopologicalSpace N] [ChartedSpace H3 N]variable [@IsManifold ℝ _ E3 _ _ H3 (@instTopologicalSpaceEuclideanHalfSpace 3 CKSBoundarySurface.halfSpaceDimension_neZero) I3 ∞ N _ _]instance domainSecondCountable [SecondCountableTopology N] (D : OAI.CKSGeometricCuts.OuterDomain N) : SecondCountableTopology D.Carrier := D.embedding.isEmbedding.secondCountableTopologyabbrev SmoothMetric := letI := OAI.CKSBoundarySurface.halfSpaceDimension_neZero letI := OAI.CKSInducedArea.tangent_vectorBundle OAI.CKSBoundarySurface.I3 (M := N) ContMDiffRiemannianMetric OAI.CKSBoundarySurface.I3 ∞ OAI.CKSBoundarySurface.E3 (fun x : N => TangentSpace OAI.CKSBoundarySurface.I3 x)def cutMetric (g : OAI.CKSFullCutArea.SmoothMetric (N := N)) (D : OAI.CKSGeometricCuts.OuterDomain N) : ContMDiffRiemannianMetric OAI.CKSBoundarySurface.I2 ∞ OAI.CKSBoundarySurface.E2 (fun x : OAI.CKSFullCutArea.Surface D => TangentSpace OAI.CKSBoundarySurface.I2 x) := have proof_boundary_chart_zero_49 {M : Type u} [instLocal1 : TopologicalSpace.{u} M] [instLocal2 : ChartedSpace.{0, u} OAI.CKSIntrinsicGeometry.H3 M] [instLocal3 : IsManifold.{0, 0, 0, u} OAI.CKSIntrinsicGeometry.I3 1 M] (x y : M) (hy : y ∈ (extChartAt OAI.CKSIntrinsicGeometry.I3 x).source) (hS : y ∈ OAI.CKSIntrinsicGeometry.I3.boundary M) : (extChartAt OAI.CKSIntrinsicGeometry.I3 x y) 0 = 0 := by have hychart : y ∈ (chartAt OAI.CKSIntrinsicGeometry.H3 x).source := by simpa using hy have hyrange : extChartAt OAI.CKSIntrinsicGeometry.I3 x y ∈ range OAI.CKSIntrinsicGeometry.I3 := (extChartAt_target_subset_range x) ((extChartAt OAI.CKSIntrinsicGeometry.I3 x).map_source hy) have hnonneg : 0 ≤ (extChartAt OAI.CKSIntrinsicGeometry.I3 x y) 0 := by simpa only [OAI.CKSIntrinsicGeometry.I3, range_modelWithCornersEuclideanHalfSpace, mem_ofPred_eq] using hyrange have hnot : ¬OAI.CKSIntrinsicGeometry.I3.IsInteriorPoint y := (OAI.CKSIntrinsicGeometry.I3.isBoundaryPoint_iff_not_isInteriorPoint y).mp hS have hle : (extChartAt OAI.CKSIntrinsicGeometry.I3 x y) 0 ≤ 0 := by by_contra h have hpos : 0 < (extChartAt OAI.CKSIntrinsicGeometry.I3 x y) 0 := lt_of_not_ge h have hint : extChartAt OAI.CKSIntrinsicGeometry.I3 x y ∈ interior (range OAI.CKSIntrinsicGeometry.I3) := by simpa only [OAI.CKSIntrinsicGeometry.I3, interior_range_modelWithCornersEuclideanHalfSpace, mem_ofPred_eq] using hpos apply hnot apply (OAI.CKSIntrinsicGeometry.I3.isInteriorPoint_iff_of_mem_atlas one_ne_zero (chart_mem_atlas OAI.CKSIntrinsicGeometry.H3 x) hychart).mpr exact (chartAt OAI.CKSIntrinsicGeometry.H3 x).mem_interior_extend_target ((chartAt OAI.CKSIntrinsicGeometry.H3 x).map_source hychart) hint exact le_antisymm hle hnonneg have proof_liftPlane_zero_6 (z : OAI.CKSBoundarySurface.E2) : OAI.CKSBoundarySurface.liftPlane z 0 = 0 := rfl have proof_liftPlane_succ_7 (z : OAI.CKSBoundarySurface.E2) (i : Fin 2) : OAI.CKSBoundarySurface.liftPlane z i.succ = z i := rfl have proof_I3_liftHalf_23 (z : OAI.CKSBoundarySurface.E2) : OAI.CKSBoundarySurface.I3 (OAI.CKSBoundarySurface.liftHalf z) = OAI.CKSBoundarySurface.liftPlane z := rfl have proof_boundary_iff_zero_50 {M : Type u} [instLocal1 : TopologicalSpace.{u} M] [instLocal2 : ChartedSpace.{0, u} OAI.CKSBoundarySurface.H3 M] [instLocal3 : IsManifold.{0, 0, 0, u} OAI.CKSBoundarySurface.I3 (∞ : ℕ∞ω) M] (x y : M) (hy : y ∈ (chartAt OAI.CKSBoundarySurface.H3 x).source) : y ∈ OAI.CKSBoundarySurface.I3.boundary M ↔ (OAI.CKSBoundarySurface.I3 (chartAt OAI.CKSBoundarySurface.H3 x y)) 0 = 0 := by constructor · exact proof_boundary_chart_zero_49 x y (by simp [*]) · intro hz apply (OAI.CKSBoundarySurface.I3.isBoundaryPoint_iff_not_isInteriorPoint y).mpr intro hi have hin := (OAI.CKSBoundarySurface.I3.isInteriorPoint_iff_of_mem_atlas (by simp [*] : (∞ : ℕ∞ω) ≠ 0) (chart_mem_atlas OAI.CKSBoundarySurface.H3 x) hy).mp hi have hr := (chartAt OAI.CKSBoundarySurface.H3 x).interior_extend_target_subset_interior_range hin have hp : 0 < (OAI.CKSBoundarySurface.I3 (chartAt OAI.CKSBoundarySurface.H3 x y)) 0 := by simpa only [OAI.CKSBoundarySurface.I3, interior_range_modelWithCornersEuclideanHalfSpace, mem_ofPred_eq, OpenPartialHomeomorph.extend_coe, Function.comp_apply] using hr rw [hz] at hp exact (lt_irrefl 0) hp have proof_chart_inverse_boundary_51 {M : Type u} [instLocal1 : TopologicalSpace.{u} M] [instLocal2 : ChartedSpace.{0, u} OAI.CKSBoundarySurface.H3 M] [instLocal3 : IsManifold.{0, 0, 0, u} OAI.CKSBoundarySurface.I3 (∞ : ℕ∞ω) M] (x : M) {z : OAI.CKSBoundarySurface.E2} (hz : OAI.CKSBoundarySurface.liftHalf z ∈ (chartAt OAI.CKSBoundarySurface.H3 x).target) : (chartAt OAI.CKSBoundarySurface.H3 x).symm (OAI.CKSBoundarySurface.liftHalf z) ∈ OAI.CKSBoundarySurface.I3.boundary M := by apply (proof_boundary_iff_zero_50 x _ ((chartAt OAI.CKSBoundarySurface.H3 x).map_target hz)).mpr rw [(chartAt OAI.CKSBoundarySurface.H3 x).right_inv hz] rfl have proof_boundaryInverse_mem_52 {M : Type u} [instLocal1 : TopologicalSpace.{u} M] [instLocal2 : ChartedSpace.{0, u} OAI.CKSBoundarySurface.H3 M] [instLocal3 : IsManifold.{0, 0, 0, u} OAI.CKSBoundarySurface.I3 (∞ : ℕ∞ω) M] (x : OAI.CKSBoundarySurface.Boundary M) {z : OAI.CKSBoundarySurface.E2} (hz : OAI.CKSBoundarySurface.liftHalf z ∈ (chartAt OAI.CKSBoundarySurface.H3 x.val).target) : (chartAt OAI.CKSBoundarySurface.H3 x.val).symm (OAI.CKSBoundarySurface.liftHalf z) ∈ OAI.CKSBoundarySurface.Boundary M := proof_chart_inverse_boundary_51 x.val hz have proof_boundaryInverse_val_53 {M : Type u} [instLocal1 : TopologicalSpace.{u} M] [instLocal2 : ChartedSpace.{0, u} OAI.CKSBoundarySurface.H3 M] [instLocal3 : IsManifold.{0, 0, 0, u} OAI.CKSBoundarySurface.I3 (∞ : ℕ∞ω) M] (x : OAI.CKSBoundarySurface.Boundary M) {z : OAI.CKSBoundarySurface.E2} (hz : OAI.CKSBoundarySurface.liftHalf z ∈ (chartAt OAI.CKSBoundarySurface.H3 x.val).target) : (OAI.CKSBoundarySurface.boundaryInverse x z).val = (chartAt OAI.CKSBoundarySurface.H3 x.val).symm (OAI.CKSBoundarySurface.liftHalf z) := by simp only [OAI.CKSBoundarySurface.boundaryInverse,dite_eq_left hz] have proof_boundaryChart_symm_val_54 {M : Type u} [instLocal1 : TopologicalSpace.{u} M] [instLocal2 : ChartedSpace.{0, u} OAI.CKSBoundarySurface.H3 M] [instLocal3 : IsManifold.{0, 0, 0, u} OAI.CKSBoundarySurface.I3 (∞ : ℕ∞ω) M] (x : OAI.CKSBoundarySurface.Boundary M) {z : OAI.CKSBoundarySurface.E2} (hz : z ∈ (OAI.CKSBoundarySurface.boundaryChart x).target) : ((OAI.CKSBoundarySurface.boundaryChart x).symm z).val = (chartAt OAI.CKSBoundarySurface.H3 x.val).symm (OAI.CKSBoundarySurface.liftHalf z) := proof_boundaryInverse_val_53 x hz have proof_inclusion_chart_formula_55 {M : Type u} [instLocal1 : TopologicalSpace.{u} M] [instLocal2 : ChartedSpace.{0, u} OAI.CKSBoundarySurface.H3 M] [instLocal3 : IsManifold.{0, 0, 0, u} OAI.CKSBoundarySurface.I3 (∞ : ℕ∞ω) M] (x : OAI.CKSBoundarySurface.Boundary M) {z : OAI.CKSBoundarySurface.E2} (hz : z ∈ (OAI.CKSBoundarySurface.boundaryChart x).target) : writtenInExtChartAt OAI.CKSBoundarySurface.I2 OAI.CKSBoundarySurface.I3 x (Subtype.val : OAI.CKSBoundarySurface.Boundary M → M) z = OAI.CKSBoundarySurface.liftPlane z := by change OAI.CKSBoundarySurface.I3 (chartAt OAI.CKSBoundarySurface.H3 x.val (((OAI.CKSBoundarySurface.boundaryChart x).symm z).val)) = _ rw [proof_boundaryChart_symm_val_54 x hz, (chartAt OAI.CKSBoundarySurface.H3 x.val).right_inv hz] rfl have proof_inclusion_chart_eventually_56 {M : Type u} [instLocal1 : TopologicalSpace.{u} M] [instLocal2 : ChartedSpace.{0, u} OAI.CKSBoundarySurface.H3 M] [instLocal3 : IsManifold.{0, 0, 0, u} OAI.CKSBoundarySurface.I3 (∞ : ℕ∞ω) M] (x : OAI.CKSBoundarySurface.Boundary M) : writtenInExtChartAt OAI.CKSBoundarySurface.I2 OAI.CKSBoundarySurface.I3 x (Subtype.val : OAI.CKSBoundarySurface.Boundary M → M) =ᶠ[𝓝 (extChartAt OAI.CKSBoundarySurface.I2 x x)] OAI.CKSBoundarySurface.liftPlane := by have ht : (OAI.CKSBoundarySurface.boundaryChart x).target ∈ 𝓝 (extChartAt OAI.CKSBoundarySurface.I2 x x) := (OAI.CKSBoundarySurface.boundaryChart x).open_target.mem_nhds ((OAI.CKSBoundarySurface.boundaryChart x).map_source (mem_chart_source OAI.CKSBoundarySurface.E2 x)) filter_upwards [ht] with z hz exact proof_inclusion_chart_formula_55 x hz have proof_inclusion_smooth_57 {M : Type u} [instLocal1 : TopologicalSpace.{u} M] [instLocal2 : ChartedSpace.{0, u} OAI.CKSBoundarySurface.H3 M] [instLocal3 : IsManifold.{0, 0, 0, u} OAI.CKSBoundarySurface.I3 (∞ : ℕ∞ω) M] : ContMDiff OAI.CKSBoundarySurface.I2 OAI.CKSBoundarySurface.I3 ∞ (Subtype.val : OAI.CKSBoundarySurface.Boundary M → M) := by intro x apply contMDiffAt_iff.mpr refine ⟨continuous_subtype_val.continuousAt, ?_⟩ exact ((OAI.CKSBoundarySurface.liftPlane.contDiff.contDiffAt).congr_of_eventuallyEq (proof_inclusion_chart_eventually_56 x)).contDiffWithinAt have proof_cutInclusion_smooth_47 {N : Type u} [instLocal1 : TopologicalSpace.{u} N] [instLocal2 : ChartedSpace.{0, u} OAI.CKSBoundarySurface.H3 N] [instLocal3 : IsManifold.{0, 0, 0, u} OAI.CKSBoundarySurface.I3 (∞ : ℕ∞ω) N] [IsManifold OAI.CKSBoundarySurface.I3 ∞ N] (D : OAI.CKSGeometricCuts.OuterDomain N) : ContMDiff OAI.CKSBoundarySurface.I2 OAI.CKSBoundarySurface.I3 ∞ (OAI.CKSFullCutArea.cutInclusion D) := D.embedding.isImmersion.contMDiff.comp proof_inclusion_smooth_57 have proof_extended_chart_derivative_injective_58 {M : Type u} [instLocal1 : TopologicalSpace.{u} M] [instLocal2 : ChartedSpace.{0, u} OAI.CKSEmbeddingDerivative.H M] [instLocal3 : IsManifold.{0, 0, 0, u} OAI.CKSEmbeddingDerivative.I (∞ : ℕ∞ω) M] [IsManifold OAI.CKSEmbeddingDerivative.I ∞ M] (e : OpenPartialHomeomorph M OAI.CKSEmbeddingDerivative.H) (he : e ∈ IsManifold.maximalAtlas OAI.CKSEmbeddingDerivative.I ∞ M) {x : M} (hx : x ∈ e.source) : Injective (mfderiv OAI.CKSEmbeddingDerivative.I 𝓘(ℝ,OAI.CKSEmbeddingDerivative.E) (e.extend OAI.CKSEmbeddingDerivative.I) x) := by have hed : e.MDifferentiable OAI.CKSEmbeddingDerivative.I OAI.CKSEmbeddingDerivative.I := ⟨ (contMDiffOn_of_mem_maximalAtlas he).mdifferentiableOn (by simp), (contMDiffOn_symm_of_mem_maximalAtlas he).mdifferentiableOn (by simp)⟩ have hcomp := mfderiv_comp x OAI.CKSEmbeddingDerivative.I.mdifferentiableAt ((hed.1 x hx).mdifferentiableAt (e.open_source.mem_nhds hx)) change mfderiv OAI.CKSEmbeddingDerivative.I 𝓘(ℝ,OAI.CKSEmbeddingDerivative.E) (e.extend OAI.CKSEmbeddingDerivative.I) x = _ at hcomp rw [OAI.CKSEmbeddingDerivative.I.hasMFDerivAt.mfderiv] at hcomp change mfderiv OAI.CKSEmbeddingDerivative.I 𝓘(ℝ,OAI.CKSEmbeddingDerivative.E) (e.extend OAI.CKSEmbeddingDerivative.I) x = mfderiv OAI.CKSEmbeddingDerivative.I OAI.CKSEmbeddingDerivative.I e x at hcomp rw [hcomp] exact hed.mfderiv_injective hx have proof_immersion_derivative_injective_59 {M : Type u} {N : Type u} [instLocal2 : TopologicalSpace.{u} M] [instLocal3 : ChartedSpace.{0, u} OAI.CKSEmbeddingDerivative.H M] [instLocal4 : IsManifold.{0, 0, 0, u} OAI.CKSEmbeddingDerivative.I (∞ : ℕ∞ω) M] [instLocal5 : TopologicalSpace.{u} N] [instLocal6 : ChartedSpace.{0, u} OAI.CKSEmbeddingDerivative.H N] [instLocal7 : IsManifold.{0, 0, 0, u} OAI.CKSEmbeddingDerivative.I (∞ : ℕ∞ω) N] [IsManifold OAI.CKSEmbeddingDerivative.I ∞ N] {f : M → N} {x : M} (h : IsImmersionAt OAI.CKSEmbeddingDerivative.I OAI.CKSEmbeddingDerivative.I ∞ f x) : Injective (mfderiv OAI.CKSEmbeddingDerivative.I OAI.CKSEmbeddingDerivative.I f x) := by let A : OAI.CKSEmbeddingDerivative.E →L[ℝ] OAI.CKSEmbeddingDerivative.E := (ContinuousLinearMap.fst ℝ OAI.CKSEmbeddingDerivative.E h.complement).comp h.equiv.symm.toContinuousLinearMap let L : N → OAI.CKSEmbeddingDerivative.E := A ∘ (h.codChart.extend OAI.CKSEmbeddingDerivative.I) have hL : ContMDiffAt OAI.CKSEmbeddingDerivative.I 𝓘(ℝ,OAI.CKSEmbeddingDerivative.E) ∞ L (f x) := A.contMDiff.contMDiffAt.comp _ (h.codChart.contMDiffAt_extend h.codChart_mem_maximalAtlas h.mem_codChart_source) have heq : (L ∘ f) =ᶠ[𝓝 x] h.domChart.extend OAI.CKSEmbeddingDerivative.I := by filter_upwards [h.domChart.open_source.mem_nhds h.mem_domChart_source] with y hy have hy' : y ∈ (h.domChart.extend OAI.CKSEmbeddingDerivative.I).source := by simpa only [OpenPartialHomeomorph.extend_source] using hy have hw := h.writtenInCharts ((h.domChart.extend OAI.CKSEmbeddingDerivative.I).map_source hy') dsimp only [Function.comp_apply] at hw rw [(h.domChart.extend OAI.CKSEmbeddingDerivative.I).left_inv hy'] at hw change A ((h.codChart.extend OAI.CKSEmbeddingDerivative.I) (f y)) = _ rw [hw] simp only [A,ContinuousLinearMap.comp_apply,ContinuousLinearEquiv.coe_coe, ContinuousLinearEquiv.symm_apply_apply ] rfl have hdL := hL.mdifferentiableAt (by simp) have hdf := h.contMDiffAt.mdifferentiableAt (by simp) have hder := heq.mfderiv_eq (I := OAI.CKSEmbeddingDerivative.I) (I' := 𝓘(ℝ,OAI.CKSEmbeddingDerivative.E)) rw [mfderiv_comp x hdL hdf] at hder change _ = mfderiv OAI.CKSEmbeddingDerivative.I 𝓘(ℝ,OAI.CKSEmbeddingDerivative.E) (h.domChart.extend OAI.CKSEmbeddingDerivative.I) x at hder have hinj := proof_extended_chart_derivative_injective_58 h.domChart h.domChart_mem_maximalAtlas h.mem_domChart_source rw [← hder] at hinj have hi' : Injective ((mfderiv OAI.CKSEmbeddingDerivative.I 𝓘(ℝ,OAI.CKSEmbeddingDerivative.E) L (f x)) ∘ (mfderiv OAI.CKSEmbeddingDerivative.I OAI.CKSEmbeddingDerivative.I f x)) := hinj exact hi'.of_comp have proof_smooth_embedding_derivative_injective_60 {M : Type u} {N : Type u} [instLocal2 : TopologicalSpace.{u} M] [instLocal3 : ChartedSpace.{0, u} OAI.CKSEmbeddingDerivative.H M] [instLocal4 : IsManifold.{0, 0, 0, u} OAI.CKSEmbeddingDerivative.I (∞ : ℕ∞ω) M] [instLocal5 : TopologicalSpace.{u} N] [instLocal6 : ChartedSpace.{0, u} OAI.CKSEmbeddingDerivative.H N] [instLocal7 : IsManifold.{0, 0, 0, u} OAI.CKSEmbeddingDerivative.I (∞ : ℕ∞ω) N] {f : M → N} (h : IsSmoothEmbedding OAI.CKSEmbeddingDerivative.I OAI.CKSEmbeddingDerivative.I ∞ f) : ∀ x, Injective (mfderiv OAI.CKSEmbeddingDerivative.I OAI.CKSEmbeddingDerivative.I f x) := fun x => proof_immersion_derivative_injective_59 (h.isImmersion.isImmersionAt x) have proof_inclusion_hasMFDeriv_61 {M : Type u} [instLocal1 : TopologicalSpace.{u} M] [instLocal2 : ChartedSpace.{0, u} OAI.CKSBoundarySurface.H3 M] [instLocal3 : IsManifold.{0, 0, 0, u} OAI.CKSBoundarySurface.I3 (∞ : ℕ∞ω) M] (x : OAI.CKSBoundarySurface.Boundary M) : HasMFDerivAt OAI.CKSBoundarySurface.I2 OAI.CKSBoundarySurface.I3 (Subtype.val : OAI.CKSBoundarySurface.Boundary M → M) x OAI.CKSBoundarySurface.liftPlane := by refine ⟨continuous_subtype_val.continuousAt, ?_⟩ exact (OAI.CKSBoundarySurface.liftPlane.hasFDerivAt.congr_of_eventuallyEq (proof_inclusion_chart_eventually_56 x)).hasFDerivWithinAt have proof_dropPlane_apply_31 (z : OAI.CKSBoundarySurface.E3) (i : Fin 2) : OAI.CKSBoundarySurface.dropPlane z i = z i.succ := rfl have proof_drop_lift_28 (z : OAI.CKSBoundarySurface.E2) : OAI.CKSBoundarySurface.dropPlane (OAI.CKSBoundarySurface.liftPlane z) = z := by ext i; rfl have proof_inclusion_mfderiv_injective_62 {M : Type u} [instLocal1 : TopologicalSpace.{u} M] [instLocal2 : ChartedSpace.{0, u} OAI.CKSBoundarySurface.H3 M] [instLocal3 : IsManifold.{0, 0, 0, u} OAI.CKSBoundarySurface.I3 (∞ : ℕ∞ω) M] (x : OAI.CKSBoundarySurface.Boundary M) : Injective (mfderiv OAI.CKSBoundarySurface.I2 OAI.CKSBoundarySurface.I3 (Subtype.val : OAI.CKSBoundarySurface.Boundary M → M) x) := by rw [(proof_inclusion_hasMFDeriv_61 x).mfderiv] intro a b h change OAI.CKSBoundarySurface.liftPlane a = OAI.CKSBoundarySurface.liftPlane b at h have hh : OAI.CKSBoundarySurface.dropPlane (OAI.CKSBoundarySurface.liftPlane a) = OAI.CKSBoundarySurface.dropPlane (OAI.CKSBoundarySurface.liftPlane b) := congrArg OAI.CKSBoundarySurface.dropPlane h change (a : OAI.CKSBoundarySurface.E2) = (b : OAI.CKSBoundarySurface.E2) exact (proof_drop_lift_28 a).symm.trans (hh.trans (proof_drop_lift_28 b)) have proof_cutInclusion_derivative_injective_48 {N : Type u} [instLocal1 : TopologicalSpace.{u} N] [instLocal2 : ChartedSpace.{0, u} OAI.CKSBoundarySurface.H3 N] [instLocal3 : IsManifold.{0, 0, 0, u} OAI.CKSBoundarySurface.I3 (∞ : ℕ∞ω) N] [IsManifold OAI.CKSBoundarySurface.I3 ∞ N] (D : OAI.CKSGeometricCuts.OuterDomain N) (x : OAI.CKSFullCutArea.Surface D) : Injective (mfderiv OAI.CKSBoundarySurface.I2 OAI.CKSBoundarySurface.I3 (OAI.CKSFullCutArea.cutInclusion D) x) := by unfold OAI.CKSFullCutArea.cutInclusion rw [mfderiv_comp x ((D.embedding.isImmersion.contMDiff x.val).mdifferentiableAt (by simp [*])) ((proof_inclusion_smooth_57 x).mdifferentiableAt (by simp [*]))] · change Injective ((mfderiv OAI.CKSBoundarySurface.I3 OAI.CKSBoundarySurface.I3 D.inclusion x.val) ∘ (mfderiv OAI.CKSBoundarySurface.I2 OAI.CKSBoundarySurface.I3 (Subtype.val : OAI.CKSFullCutArea.Surface D → D.Carrier) x)) exact (proof_smooth_embedding_derivative_injective_60 D.embedding x.val).comp (proof_inclusion_mfderiv_injective_62 x) @OAI.CKSInducedArea.inducedMetric OAI.CKSBoundarySurface.H3 (@instTopologicalSpaceEuclideanHalfSpace 3 OAI.CKSBoundarySurface.halfSpaceDimension_neZero) OAI.CKSBoundarySurface.I3 N _ _ _ (OAI.CKSFullCutArea.Surface D) _ _ _ g (OAI.CKSFullCutArea.cutInclusion D) (proof_cutInclusion_smooth_47 D) (proof_cutInclusion_derivative_injective_48 D)end OAI.CKSFullCutAreaendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSFullCutAreaopen Set Manifold Bundle MeasureTheoryopen scoped ContDiff Topology ENNRealopen CKSGeometricCuts (OuterDomain)open CKSBoundarySurfacevariable {N : Type u} [TopologicalSpace N] [ChartedSpace H3 N] [@IsManifold ℝ _ E3 _ _ H3 (@instTopologicalSpaceEuclideanHalfSpace 3 CKSBoundarySurface.halfSpaceDimension_neZero) I3 ∞ N _ _] [SecondCountableTopology N]def area (g : OAI.CKSFullCutArea.SmoothMetric (N := N)) (D : OAI.CKSGeometricCuts.OuterDomain N) : ℝ≥0∞ := letI : MeasurableSpace (OAI.CKSFullCutArea.Surface D) := borel (OAI.CKSFullCutArea.Surface D) letI : BorelSpace (OAI.CKSFullCutArea.Surface D) := ⟨rfl⟩ OAI.CKSSurfaceVolume.riemannianVolume (OAI.CKSFullCutArea.cutMetric g D).toContinuousRiemannianMetric univdef minEnclosingArea (g : OAI.CKSFullCutArea.SmoothMetric (N := N)) : ℝ≥0∞ := ⨅ D : OAI.CKSGeometricCuts.OuterDomain N, OAI.CKSFullCutArea.area g Dend OAI.CKSFullCutAreaendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSIntrinsicConstraintsopen Set Manifold Bundle MeasureTheory CKSLorentz CKSMetricGluingopen scoped ContDiff Topology ENNRealvariable {M : Type*} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I ∞ M] [MeasurableSpace M] [BorelSpace M] [SecondCountableTopology M]local instance eight_atLeastTwo : Nat.AtLeastTwo 8 := inferInstanceend OAI.CKSIntrinsicConstraintsendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSIntrinsicConstraintsopen Set Manifold Bundle MeasureTheory CKSLorentz CKSMetricGluingopen scoped ContDiff Topology ENNRealvariable {M : Type u_1} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I ∞ M] [MeasurableSpace M] [BorelSpace M] [SecondCountableTopology M]attribute [local instance] eight_atLeastTwodef IntegrableConstraints (g : OAI.CKSMetricGluing.SmoothMetric OAI.CKSIntrinsicConstraints.I (M := M)) (K : OAI.CKSMetricGluing.InnerField OAI.CKSIntrinsicConstraints.I (M := M)) : Prop := ∃ μ j : M → ℝ, Continuous μ ∧ Continuous j ∧ Integrable μ (OAI.CKSIntrinsicVolume.riemannianVolume g.toContinuousRiemannianMetric) ∧ Integrable j (OAI.CKSIntrinsicVolume.riemannianVolume g.toContinuousRiemannianMetric) ∧ (∀ x, 0 ≤ j x ∧ j x ≤ μ x) ∧ ∀ x (c : OAI.CKSIntrinsicConstraints.ConstraintChart g.inner K x), 8 * Real.pi * μ x = c.energy ∧ 8 * Real.pi * j x = c.momentumNormend OAI.CKSIntrinsicConstraintsendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSSourceExterioropen Set Manifold Bundle CKSLorentz CKSMetricGluing CKSSpatialManifold CKSGeometricCuts CKSSphericalHarmonicsopen scoped ContDiff Topologyvariable {N : Type u} [TopologicalSpace N] [ChartedSpace H3 N] [IsManifold I3 ∞ N]local instance id_invPair (Scalar : Type u_1) [Semiring Scalar] : RingHomInvPair (RingHom.id Scalar) (RingHom.id Scalar) := inferInstancelocal instance source_manifold_one : IsManifold OAI.CKSGeometricCuts.I3 1 N := inferInstanceend OAI.CKSSourceExteriorendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSSourceExterioropen Set Manifold Bundle CKSLorentz CKSMetricGluing CKSSpatialManifold CKSGeometricCuts CKSSphericalHarmonicsopen scoped ContDiff Topologyvariable {N : Type u} [TopologicalSpace N] [ChartedSpace H3 N] [IsManifold I3 ∞ N]attribute [local instance] CKSGeometricCuts.halfSpaceDimension_neZero id_invPair source_manifold_onelocal instance source_trivialization_isLinear (point : N) : (trivializationAt OAI.CKSLorentz.E (TangentSpace OAI.CKSGeometricCuts.I3) point).IsLinear ℝ := inferInstanceend OAI.CKSSourceExteriorendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSSourceExterioropen Set Manifold Bundle CKSLorentz CKSMetricGluing CKSSpatialManifold CKSGeometricCuts CKSSphericalHarmonicsopen scoped ContDiff Topologyvariable {N : Type u} [TopologicalSpace N] [ChartedSpace H3 N] [IsManifold I3 ∞ N]attribute [local instance] CKSGeometricCuts.halfSpaceDimension_neZero id_invPair source_manifold_oneattribute [local instance] source_trivialization_isLineardef Orientable : Prop := ∃ o : ∀ x : N, Orientation ℝ (TangentSpace OAI.CKSGeometricCuts.I3 x) (Fin 3), ∀ x : N, let e := trivializationAt OAI.CKSLorentz.E (TangentSpace OAI.CKSGeometricCuts.I3) x ∃ V : Set N, IsOpen V ∧ ∃ hx : x ∈ V, ∃ hV : V ⊆ e.baseSet, ∀ y (hy : y ∈ V), let atPoint : TangentSpace OAI.CKSGeometricCuts.I3 y ≃L[ℝ] OAI.CKSLorentz.E := e.continuousLinearEquivAt ℝ y (hV hy) let atBase : TangentSpace OAI.CKSGeometricCuts.I3 x ≃L[ℝ] OAI.CKSLorentz.E := e.continuousLinearEquivAt ℝ x (hV hx) Orientation.map (Fin 3) atPoint.toLinearEquiv (o y) = Orientation.map (Fin 3) atBase.toLinearEquiv (o x)structure CoordinateEnd where radius : ℝ radius_pos : 0 < radius domain : Set N isOpen : IsOpen domain coordinate : N → OAI.CKSLorentz.E inverse : OAI.CKSLorentz.E → N smooth : ContMDiffOn OAI.CKSGeometricCuts.I3 𝓘(ℝ,OAI.CKSLorentz.E) ∞ coordinate domain inverse_smooth : ContMDiffOn 𝓘(ℝ,OAI.CKSLorentz.E) OAI.CKSGeometricCuts.I3 ∞ inverse {y | radius < ‖y‖} mapsTo : ∀ x ∈ domain, radius < ‖coordinate x‖ left_inverse : ∀ x ∈ domain, inverse (coordinate x) = x right_inverse : ∀ y, radius < ‖y‖ → inverse y ∈ domain ∧ coordinate (inverse y) = y closed_far_side : ∀ r, radius < r → IsClosed {x : N | x ∈ domain ∧ r ≤ ‖coordinate x‖} compact_inner_side : ∀ r, radius < r → IsCompact {x : N | x ∉ domain ∨ ‖coordinate x‖ ≤ r}structure CKSData (g : OAI.CKSMetricGluing.SmoothMetric OAI.CKSGeometricCuts.I3 (M := N)) (K : OAI.CKSMetricGluing.InnerField OAI.CKSGeometricCuts.I3 (M := N)) where chart : OAI.CKSSourceExterior.CoordinateEnd (N := N) metricPerturbation : OAI.CKSLorentz.SpatialTensor tensorPerturbation : OAI.CKSLorentz.SpatialTensor metric_smooth : ∀ y, chart.radius < ‖y‖ → ContDiffAt ℝ ∞ metricPerturbation y tensor_smooth : ∀ y, chart.radius < ‖y‖ → ContDiffAt ℝ ∞ tensorPerturbation y represents : ∀ x ∈ chart.domain, g.inner x = OAI.CKSSpatialManifold.endInner OAI.CKSGeometricCuts.I3 chart.coordinate (OAI.CKSLorentz.sourceSpatial metricPerturbation) x ∧ K x = OAI.CKSSpatialManifold.endInner OAI.CKSGeometricCuts.I3 chart.coordinate (OAI.CKSLorentz.sourceSpatial tensorPerturbation) x massAspect : OAI.CKSLorentz.Sphere → ℝ aspect_smooth : OAI.CKSSphericalHarmonics.SmoothSphere massAspect patches : OAI.CKSLorentz.Sphere → OAI.CKSLorentz.CKSTensorPatch covers : ∀ n, n ∈ (patches n).patch.sphereRegion (patches n).region realizes : ∀ n, (patches n).Realizes metricPerturbation tensorPerturbation aspect_eq : ∀ n, (patches n).RepresentsMassAspect massAspectend OAI.CKSSourceExteriorendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSSchwarzschildopen Set Filter Manifold Bundle MeasureTheoryopen scoped ContDiff Topology InnerProductSpace ENNRealopen CKSBoundarySurface CKSFullCutArea CKSSurfaceVolumeinstance exteriorConnected : ConnectedSpace OAI.CKSSchwarzschild.Exterior := by have : ConnectedSpace OAI.CKSSchwarzschild.Radial := isConnected_iff_connectedSpace.mp isConnected_Ici have : ConnectedSpace OAI.CKSSchwarzschild.Sphere := isConnected_iff_connectedSpace.mp (isConnected_sphere (by rw [← Module.finrank_eq_rank]; norm_num : 1 < Module.rank ℝ E3) (0 : OAI.CKSBoundarySurface.E3) (by norm_num : (0 : ℝ) ≤ 1)) infer_instanceend OAI.CKSSchwarzschildendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSSourceExterioropen Set Manifold Bundle MeasureTheory CKSGeometricCuts CKSMetricGluingopen scoped ContDiffvariable {N : Type u_1} [TopologicalSpace N] [ChartedSpace H3 N] [@IsManifold ℝ _ E3 _ _ H3 (@instTopologicalSpaceEuclideanHalfSpace 3 CKSGeometricCuts.halfSpaceDimension_neZero) I3 ∞ N _ _] [SecondCountableTopology N]def cutArea (g : @OAI.CKSMetricGluing.SmoothMetric OAI.CKSGeometricCuts.E3 _ _ OAI.CKSGeometricCuts.H3 (@instTopologicalSpaceEuclideanHalfSpace 3 OAI.CKSGeometricCuts.halfSpaceDimension_neZero) OAI.CKSGeometricCuts.I3 N _ _ _) (D : OAI.CKSGeometricCuts.OuterDomain N) : ℝ := (OAI.CKSFullCutArea.area g D).toRealdef minimumEnclosingArea (g : @OAI.CKSMetricGluing.SmoothMetric OAI.CKSGeometricCuts.E3 _ _ OAI.CKSGeometricCuts.H3 (@instTopologicalSpaceEuclideanHalfSpace 3 OAI.CKSGeometricCuts.halfSpaceDimension_neZero) OAI.CKSGeometricCuts.I3 N _ _ _) : ℝ := ⨅ D : OAI.CKSGeometricCuts.OuterDomain N, OAI.CKSSourceExterior.cutArea g Ddef constraintsIntegrable (g : OAI.CKSMetricGluing.SmoothMetric OAI.CKSGeometricCuts.I3 (M := N)) (K : OAI.CKSMetricGluing.InnerField OAI.CKSGeometricCuts.I3 (M := N)) : Prop := letI : MeasurableSpace N := borel N letI : BorelSpace N := ⟨rfl⟩ OAI.CKSIntrinsicConstraints.IntegrableConstraints g Kend OAI.CKSSourceExteriorendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSSchwarzschildopen Manifold Bundle Set Filteropen scoped ContDiff Topology InnerProductSpaceopen CKSBoundarySurfacevariable {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V]def covariantPair (g : letI := OAI.CKSLorentz.real_continuousAdd letI := OAI.CKSLorentz.real_continuousConstSMul letI := OAI.CKSLorentz.real_smulCommClass V → V →L[ℝ] V →L[ℝ] ℝ) (N : V → V) (x a b : V) : ℝ := letI := OAI.CKSLorentz.two_atLeastTwo g x (fderiv ℝ N x a) b + 1/2 * (fderiv ℝ (fun y => g y (N x) b) x a + fderiv ℝ (fun y => g y a b) x (N x) - fderiv ℝ (fun y => g y a (N x)) x b)end OAI.CKSSchwarzschildendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSSchwarzschildopen Set Filter Manifold Bundleopen scoped ContDiff Topology InnerProductSpaceopen CKSBoundarySurfaceabbrev Spacetime := ℝ × OAI.CKSBoundarySurface.E3abbrev SpacetimeBilinear := letI := OAI.CKSLorentz.real_continuousAdd letI := OAI.CKSLorentz.real_smulCommClass letI := OAI.CKSLorentz.real_continuousConstSMul OAI.CKSSchwarzschild.Spacetime →L[ℝ] OAI.CKSSchwarzschild.Spacetime →L[ℝ] ℝdef timeForm : OAI.CKSSchwarzschild.Spacetime →L[ℝ] ℝ := ContinuousLinearMap.fst ℝ ℝ OAI.CKSBoundarySurface.E3def spacePart : OAI.CKSSchwarzschild.Spacetime →L[ℝ] OAI.CKSBoundarySurface.E3 := ContinuousLinearMap.snd ℝ ℝ OAI.CKSBoundarySurface.E3def radiusForm (x : OAI.CKSBoundarySurface.E3) : OAI.CKSSchwarzschild.Spacetime →L[ℝ] ℝ := (OAI.CKSSchwarzschild.euclideanForm (OAI.CKSSchwarzschild.radialUnit x)).comp OAI.CKSSchwarzschild.spacePartdef schwarzschildH (m r : ℝ) : ℝ := letI := OAI.CKSLorentz.two_atLeastTwo 1-2*m/rlocal instance spacetimeDual_continuousAdd : ContinuousAdd (OAI.CKSSchwarzschild.Spacetime →L[ℝ] ℝ) := inferInstancelocal instance spacetimeDual_isTopologicalAddGroup : IsTopologicalAddGroup (OAI.CKSSchwarzschild.Spacetime →L[ℝ] ℝ) := inferInstancelocal instance spacetimeDual_smulCommClass : SMulCommClass ℝ ℝ (OAI.CKSSchwarzschild.Spacetime →L[ℝ] ℝ) := inferInstancelocal instance spacetimeDual_continuousConstSMul : ContinuousConstSMul ℝ (OAI.CKSSchwarzschild.Spacetime →L[ℝ] ℝ) := inferInstancelocal instance spacetimeDual_isScalarTower : IsScalarTower ℝ ℝ (OAI.CKSSchwarzschild.Spacetime →L[ℝ] ℝ) := inferInstancelocal instance spacetimeDual_continuousSMul : ContinuousSMul ℝ (OAI.CKSSchwarzschild.Spacetime →L[ℝ] ℝ) := inferInstancedef advancedMetric (m : ℝ) (z : OAI.CKSSchwarzschild.Spacetime) : OAI.CKSSchwarzschild.SpacetimeBilinear := letI := OAI.CKSLorentz.real_continuousAdd letI := OAI.CKSLorentz.real_continuousConstSMul letI := OAI.CKSLorentz.real_smulCommClass letI := OAI.CKSLorentz.real_isTopologicalAddGroup letI := OAI.CKSSchwarzschild.spacetimeDual_continuousAdd letI := OAI.CKSSchwarzschild.spacetimeDual_isTopologicalAddGroup letI := OAI.CKSSchwarzschild.spacetimeDual_smulCommClass letI := OAI.CKSSchwarzschild.spacetimeDual_continuousConstSMul letI := OAI.CKSSchwarzschild.spacetimeDual_isScalarTower letI := OAI.CKSSchwarzschild.spacetimeDual_continuousSMul letI := OAI.CKSSpatialManifold.real_id_compTriple letI := OAI.CKSSpatialManifold.real_id_isometric let spatialMetric : OAI.CKSSchwarzschild.SpacetimeBilinear := OAI.CKSSchwarzschild.euclideanForm.bilinearComp OAI.CKSSchwarzschild.spacePart OAI.CKSSchwarzschild.spacePart (-OAI.CKSSchwarzschild.schwarzschildH m ‖z.2‖) • OAI.CKSSchwarzschild.timeForm.smulRight OAI.CKSSchwarzschild.timeForm + OAI.CKSSchwarzschild.timeForm.smulRight (OAI.CKSSchwarzschild.radiusForm z.2) + (OAI.CKSSchwarzschild.radiusForm z.2).smulRight OAI.CKSSchwarzschild.timeForm + spatialMetric - (OAI.CKSSchwarzschild.radiusForm z.2).smulRight (OAI.CKSSchwarzschild.radiusForm z.2)def advancedSlope (m r : ℝ) : ℝ := (OAI.CKSSchwarzschild.lapse m r*(OAI.CKSSchwarzschild.lapse m r-OAI.CKSSchwarzschild.velocity m r))⁻¹def advancedTime (m r : ℝ) : ℝ := letI := OAI.CKSLorentz.two_atLeastTwo ∫ s in (2*m)..r, OAI.CKSSchwarzschild.advancedSlope m sdef advancedGraph (m : ℝ) (x : OAI.CKSBoundarySurface.E3) : OAI.CKSSchwarzschild.Spacetime := (OAI.CKSSchwarzschild.advancedTime m ‖x‖,x)def futureNormal (m : ℝ) (z : OAI.CKSSchwarzschild.Spacetime) : OAI.CKSSchwarzschild.Spacetime := ((OAI.CKSSchwarzschild.lapse m ‖z.2‖-OAI.CKSSchwarzschild.velocity m ‖z.2‖)⁻¹,OAI.CKSSchwarzschild.velocity m ‖z.2‖ • OAI.CKSSchwarzschild.radialUnit z.2)def graphTangent (m : ℝ) (x a : OAI.CKSBoundarySurface.E3) : OAI.CKSSchwarzschild.Spacetime := letI := OAI.CKSLorentz.two_atLeastTwo letI : Inner ℝ OAI.CKSBoundarySurface.E3 := @InnerProductSpace.toInner ℝ OAI.CKSBoundarySurface.E3 _ (PiLp.seminormedAddCommGroup 2 (fun _ : Fin 3 => ℝ)) (PiLp.innerProductSpace (fun _ : Fin 3 => ℝ)) (OAI.CKSSchwarzschild.advancedSlope m ‖x‖ * ⟪OAI.CKSSchwarzschild.radialUnit x,a⟫_ℝ,a)end OAI.CKSSchwarzschildendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSSchwarzschildopen Set Filter Manifold Bundle CKSSpatialManifold CKSMetricGluing CKSLorentzopen scoped ContDiff Topology InnerProductSpaceopen CKSBoundarySurfacestructure HorizonRegularGraph (m : ℝ) : Prop where ambient_smooth : ∀ z : OAI.CKSSchwarzschild.Spacetime, z.2 ≠ 0 → ContDiffAt ℝ ∞ (OAI.CKSSchwarzschild.advancedMetric m) z ambient_symmetric : ∀ z a b, OAI.CKSSchwarzschild.advancedMetric m z a b = OAI.CKSSchwarzschild.advancedMetric m z b a ambient_nondegenerate : ∀ z : OAI.CKSSchwarzschild.Spacetime, z.2 ≠ 0 → ∀ a : OAI.CKSSchwarzschild.Spacetime, (∀ b, OAI.CKSSchwarzschild.advancedMetric m z a b = 0) → a = 0 graph_smooth_across : ∀ x : OAI.CKSBoundarySurface.E3, m < ‖x‖ → ContDiffAt ℝ ∞ (OAI.CKSSchwarzschild.advancedGraph m) x graph_injective : Function.Injective (OAI.CKSSchwarzschild.advancedGraph m) graph_derivative : ∀ x : OAI.CKSBoundarySurface.E3, m < ‖x‖ → ∀ a, fderiv ℝ (OAI.CKSSchwarzschild.advancedGraph m) x a = OAI.CKSSchwarzschild.graphTangent m x a horizon_time : OAI.CKSSchwarzschild.advancedTime m (2*m) = 0 horizon_slope : OAI.CKSSchwarzschild.advancedSlope m (2*m) = 1/2 induced_metric : ∀ x : OAI.CKSBoundarySurface.E3, 2*m ≤ ‖x‖ → ∀ a b, OAI.CKSSchwarzschild.advancedMetric m (OAI.CKSSchwarzschild.advancedGraph m x) (OAI.CKSSchwarzschild.graphTangent m x a) (OAI.CKSSchwarzschild.graphTangent m x b) = OAI.CKSSchwarzschild.cartMetric m x a b normal_unit : ∀ x : OAI.CKSBoundarySurface.E3, 2*m ≤ ‖x‖ → OAI.CKSSchwarzschild.advancedMetric m (OAI.CKSSchwarzschild.advancedGraph m x) (OAI.CKSSchwarzschild.futureNormal m (OAI.CKSSchwarzschild.advancedGraph m x)) (OAI.CKSSchwarzschild.futureNormal m (OAI.CKSSchwarzschild.advancedGraph m x)) = -1 normal_orthogonal : ∀ x : OAI.CKSBoundarySurface.E3, 2*m ≤ ‖x‖ → ∀ a, OAI.CKSSchwarzschild.advancedMetric m (OAI.CKSSchwarzschild.advancedGraph m x) (OAI.CKSSchwarzschild.futureNormal m (OAI.CKSSchwarzschild.advancedGraph m x)) (OAI.CKSSchwarzschild.graphTangent m x a) = 0 future_facing : ∀ x : OAI.CKSBoundarySurface.E3, 2*m ≤ ‖x‖ → 0 < (OAI.CKSSchwarzschild.futureNormal m (OAI.CKSSchwarzschild.advancedGraph m x)).1 induced_second_form : ∀ x : OAI.CKSBoundarySurface.E3, 2*m ≤ ‖x‖ → ∀ a b, OAI.CKSSchwarzschild.covariantPair (OAI.CKSSchwarzschild.advancedMetric m) (OAI.CKSSchwarzschild.futureNormal m) (OAI.CKSSchwarzschild.advancedGraph m x) (OAI.CKSSchwarzschild.graphTangent m x a) (OAI.CKSSchwarzschild.graphTangent m x b) = OAI.CKSSchwarzschild.cartTensor m x a bend OAI.CKSSchwarzschildendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSSchwarzschildopen Set Filter Manifold Bundleopen scoped ContDiff Topology InnerProductSpaceopen CKSBoundarySurfaceattribute [local instance] CKSInducedArea.real_continuousAdd CKSInducedArea.real_smulCommClass CKSInducedArea.real_continuousConstSMul CKSBoundarySurface.two_atLeastTwolocal instance frameCovectorModule : Module ℝ (OAI.CKSBoundarySurface.E3 →L[ℝ] ℝ) := @ContinuousLinearMap.module ℝ ℝ ℝ _ _ _ OAI.CKSBoundarySurface.E3 _ _ _ ℝ _ _ _ _ OAI.CKSInducedArea.real_smulCommClass OAI.CKSInducedArea.real_continuousConstSMul (RingHom.id ℝ) OAI.CKSInducedArea.real_continuousAddend OAI.CKSSchwarzschildendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSSchwarzschildopen Set Filter Manifold Bundleopen scoped ContDiff Topology InnerProductSpaceopen CKSBoundarySurfaceattribute [local instance] CKSInducedArea.real_continuousAdd CKSInducedArea.real_smulCommClass CKSInducedArea.real_continuousConstSMul CKSBoundarySurface.two_atLeastTwoattribute [local instance] OAI.CKSSchwarzschild.frameCovectorModuledef christoffelPair (g : OAI.CKSBoundarySurface.E3 → OAI.CKSBoundarySurface.E3 →L[ℝ] OAI.CKSBoundarySurface.E3 →L[ℝ] ℝ) (x a b c : OAI.CKSBoundarySurface.E3) : ℝ := 1/2 * (fderiv ℝ (fun z => g z b c) x a + fderiv ℝ (fun z => g z a c) x b - fderiv ℝ (fun z => g z a b) x c)def firstFrame (g : OAI.CKSBoundarySurface.E3 →L[ℝ] OAI.CKSBoundarySurface.E3 →L[ℝ] ℝ) (T : OAI.CKSBoundarySurface.E2 →L[ℝ] OAI.CKSBoundarySurface.E3) : OAI.CKSBoundarySurface.E2 := (Real.sqrt (g (T (EuclideanSpace.single 0 1)) (T (EuclideanSpace.single 0 1))))⁻¹ • EuclideanSpace.single 0 1def secondResidual (g : OAI.CKSBoundarySurface.E3 →L[ℝ] OAI.CKSBoundarySurface.E3 →L[ℝ] ℝ) (T : OAI.CKSBoundarySurface.E2 →L[ℝ] OAI.CKSBoundarySurface.E3) : OAI.CKSBoundarySurface.E2 := EuclideanSpace.single 1 1 - (g (T (EuclideanSpace.single 0 1)) (T (EuclideanSpace.single 1 1)) / g (T (EuclideanSpace.single 0 1)) (T (EuclideanSpace.single 0 1))) • EuclideanSpace.single 0 1def secondFrame (g : OAI.CKSBoundarySurface.E3 →L[ℝ] OAI.CKSBoundarySurface.E3 →L[ℝ] ℝ) (T : OAI.CKSBoundarySurface.E2 →L[ℝ] OAI.CKSBoundarySurface.E3) : OAI.CKSBoundarySurface.E2 := (Real.sqrt (g (T (OAI.CKSSchwarzschild.secondResidual g T)) (T (OAI.CKSSchwarzschild.secondResidual g T))))⁻¹ • OAI.CKSSchwarzschild.secondResidual g Tend OAI.CKSSchwarzschildendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSSourceExterioropen Manifold CKSGeometricCutsopen scoped ContDiffvariable {N : Type*} [TopologicalSpace N] [ChartedSpace H3 N]local instance halfSpace_locallyCompact : LocallyCompactSpace OAI.CKSGeometricCuts.H3 := by change LocallyCompactSpace {x : EuclideanSpace ℝ (Fin 3) // 0 ≤ x 0} have hc : IsClosed {x : EuclideanSpace ℝ (Fin 3) | 0 ≤ x 0} := isClosed_le continuous_const (by fun_prop) exact hc.locallyCompactSpaceend OAI.CKSSourceExteriorendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSSourceExterioropen Manifold CKSGeometricCutsopen scoped ContDiffvariable {N : Type u_1} [TopologicalSpace N] [ChartedSpace H3 N]local instance manifold_regular [IsManifold OAI.CKSGeometricCuts.I3 ∞ N] [T2Space N] : T3Space N := by let := OAI.CKSSourceExterior.halfSpace_locallyCompact let : LocallyCompactSpace N := ChartedSpace.locallyCompactSpace OAI.CKSGeometricCuts.H3 N infer_instanceend OAI.CKSSourceExteriorendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSSourceExterioropen Set Manifold Bundle Filter CKSLorentz CKSMetricGluing CKSSpatialManifold CKSGeometricCutsopen CKSADM (Symbol)open scoped ContDiff Topologyvariable {N : Type u_1} [TopologicalSpace N] [ChartedSpace H3 N] [IsManifold I3 ∞ N] [T2Space N] [SecondCountableTopology N] [ConnectedSpace N]attribute [local instance] manifold_regulartheorem area_controlled_end_replacement (g : OAI.CKSMetricGluing.SmoothMetric OAI.CKSGeometricCuts.I3 (M := N)) (K : OAI.CKSMetricGluing.InnerField OAI.CKSGeometricCuts.I3 (M := N)) (hK : ContMDiff OAI.CKSGeometricCuts.I3 (OAI.CKSGeometricCuts.I3.prod 𝓘(ℝ,OAI.CKSLorentz.SpatialBilinear)) ∞ (OAI.CKSMetricGluing.innerSection OAI.CKSGeometricCuts.I3 K)) (hKsym : ∀ x v w, K x v w = K x w v) (hOrient : OAI.CKSSourceExterior.Orientable (N := N)) (hScompact : IsCompact (OAI.CKSGeometricCuts.I3.boundary N)) (hSnonempty : (OAI.CKSGeometricCuts.I3.boundary N).Nonempty) (hcomplete : OAI.CKSReplacementCompleteness.IsComplete OAI.CKSGeometricCuts.I3 g.toContinuousRiemannianMetric) (hDEC : OAI.CKSSpatialManifold.PhysicalDEC OAI.CKSGeometricCuts.I3 g.inner K) (d : OAI.CKSSourceExterior.CKSData g K) (ht : ‖(OAI.CKSLorentz.bondiCharge d.massAspect).2‖ < (OAI.CKSLorentz.bondiCharge d.massAspect).1) : ∃ (d' : OAI.CKSSourceExterior.CKSData g K) (R₀ : ℝ) (ε : ℝ → ℝ), OAI.CKSLorentz.bondiCharge d'.massAspect = (Real.sqrt ((OAI.CKSLorentz.bondiCharge d.massAspect).1^2 - ‖(OAI.CKSLorentz.bondiCharge d.massAspect).2‖^2),0) ∧ d'.chart.radius < R₀ ∧ 12 ≤ R₀ ∧ Tendsto ε atTop (𝓝 0) ∧ OAI.CKSFullCutArea.minEnclosingArea g < ⊤ ∧ ∀ R ≥ R₀, (0 ≤ ε R ∧ ε R < 1) ∧ ∃ (gR : OAI.CKSMetricGluing.SmoothMetric OAI.CKSGeometricCuts.I3 (M := N)) (kR : OAI.CKSMetricGluing.InnerField OAI.CKSGeometricCuts.I3 (M := N)) (G k : OAI.CKSLorentz.SpatialTensor) (η : ℝ), ContMDiff OAI.CKSGeometricCuts.I3 (OAI.CKSGeometricCuts.I3.prod 𝓘(ℝ,OAI.CKSLorentz.SpatialBilinear)) ∞ (OAI.CKSMetricGluing.innerSection OAI.CKSGeometricCuts.I3 kR) ∧ (∀ x v w, kR x v w = kR x w v) ∧ (∀ x, x ∉ d'.chart.domain ∨ ‖d'.chart.coordinate x‖ ≤ R → gR.inner x = g.inner x ∧ kR x = K x) ∧ OAI.CKSSpatialManifold.PhysicalDEC OAI.CKSGeometricCuts.I3 gR.inner kR ∧ (∀ x v, (1-ε R) * g.inner x v v ≤ gR.inner x v v) ∧ OAI.CKSReplacementCompleteness.IsComplete OAI.CKSGeometricCuts.I3 gR.toContinuousRiemannianMetric ∧ OAI.CKSSourceExterior.constraintsIntegrable gR kR ∧ (∀ x ∈ d'.chart.domain, gR.inner x = OAI.CKSSpatialManifold.endInner OAI.CKSGeometricCuts.I3 d'.chart.coordinate G x ∧ kR x = OAI.CKSSpatialManifold.endInner OAI.CKSGeometricCuts.I3 d'.chart.coordinate k x) ∧ (∀ i j : Fin 3, OAI.CKSADM.Symbol 1 (fun x => OAI.CKSLorentz.spatialCartesian G x i j - (if i=j then 1 else 0))) ∧ (∀ x : OAI.CKSLorentz.E, 2*R^2 < ‖x‖ → k x = 0) ∧ Tendsto (OAI.CKSLorentz.spatialADMEnergy G) atTop (𝓝 (Real.sqrt ((OAI.CKSLorentz.bondiCharge d.massAspect).1^2 - ‖(OAI.CKSLorentz.bondiCharge d.massAspect).2‖^2) + η)) ∧ Tendsto (OAI.CKSLorentz.spatialADMMomentum G k) atTop (𝓝 0) ∧ 0 ≤ η ∧ η ≤ 2 * R ^ (-(1/2 : ℝ)) ∧ OAI.CKSFullCutArea.minEnclosingArea gR < ⊤ ∧ (1-ε R) * OAI.CKSSourceExterior.minimumEnclosingArea g ≤ OAI.CKSSourceExterior.minimumEnclosingArea gR ∧ ∀ D : OAI.CKSGeometricCuts.OuterDomain N, OAI.CKSFullCutArea.area g D < ⊤ ∧ OAI.CKSFullCutArea.area gR D < ⊤ ∧ (1-ε R) * OAI.CKSSourceExterior.cutArea g D ≤ OAI.CKSSourceExterior.cutArea gR D := by sorryend OAI.CKSSourceExteriorendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSMainopen Set Filter Manifold Bundle CKSLorentz CKSMetricGluing CKSSpatialManifoldopen CKSBoundarySurface CKSIntrinsicConstraints CKSSourceExterioropen scoped ContDiff Topologyattribute [local instance] manifold_regulardef secondForm (q : OAI.CKSLorentz.SpatialTensor) (f : OAI.CKSBoundarySurface.E2 → OAI.CKSBoundarySurface.E3) (y : OAI.CKSBoundarySurface.E2) (ν : OAI.CKSBoundarySurface.E3) (a b : OAI.CKSBoundarySurface.E2) : ℝ := -(q (f y) ν (fderiv ℝ (fun z => fderiv ℝ f z b) y a) + OAI.CKSSchwarzschild.christoffelPair q (f y) (fderiv ℝ f y a) (fderiv ℝ f y b) ν)def meanCurvature (q : OAI.CKSLorentz.SpatialTensor) (f : OAI.CKSBoundarySurface.E2 → OAI.CKSBoundarySurface.E3) (y : OAI.CKSBoundarySurface.E2) (ν : OAI.CKSBoundarySurface.E3) : ℝ := let a := OAI.CKSSchwarzschild.firstFrame (q (f y)) (fderiv ℝ f y) let b := OAI.CKSSchwarzschild.secondFrame (q (f y)) (fderiv ℝ f y) OAI.CKSMain.secondForm q f y ν a a + OAI.CKSMain.secondForm q f y ν b bdef tangentialTrace (q k : OAI.CKSLorentz.SpatialTensor) (f : OAI.CKSBoundarySurface.E2 → OAI.CKSBoundarySurface.E3) (y : OAI.CKSBoundarySurface.E2) : ℝ := let a := fderiv ℝ f y (OAI.CKSSchwarzschild.firstFrame (q (f y)) (fderiv ℝ f y)) let b := fderiv ℝ f y (OAI.CKSSchwarzschild.secondFrame (q (f y)) (fderiv ℝ f y)) k (f y) a a + k (f y) b bend OAI.CKSMainendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSMainopen Set Filter Manifold Bundle CKSLorentz CKSMetricGluing CKSSpatialManifoldopen CKSBoundarySurface CKSIntrinsicConstraints CKSSourceExterioropen scoped ContDiff Topologyattribute [local instance] manifold_regularvariable {N : Type u} [TopologicalSpace N] [ChartedSpace H3 N] [IsManifold I3 ∞ N]structure BoundaryGeometry (q : OAI.CKSMetricGluing.SmoothMetric OAI.CKSBoundarySurface.I3 (M := N)) (k : OAI.CKSMetricGluing.InnerField OAI.CKSBoundarySurface.I3 (M := N)) where normal : ∀ p : OAI.CKSBoundarySurface.Boundary N, TangentSpace OAI.CKSBoundarySurface.I3 p.val unit : ∀ p, q.inner p.val (normal p) (normal p) = 1 orthogonal : ∀ p a, q.inner p.val (normal p) (mfderiv OAI.CKSBoundarySurface.I2 OAI.CKSBoundarySurface.I3 (Subtype.val : OAI.CKSBoundarySurface.Boundary N → N) p a) = 0 inward : ∀ p, 0 < (show OAI.CKSBoundarySurface.E3 from normal p) 0 chart : ∀ p : OAI.CKSBoundarySurface.Boundary N, OAI.CKSIntrinsicConstraints.ConstraintChart q.inner k p.val normal_smooth : ∀ p, ContMDiffAt OAI.CKSBoundarySurface.I2 𝓘(ℝ,OAI.CKSBoundarySurface.E3) ∞ (fun z : OAI.CKSBoundarySurface.Boundary N => mfderiv OAI.CKSBoundarySurface.I3 𝓘(ℝ,OAI.CKSBoundarySurface.E3) (chart p).coordinate z.val (normal z)) pdef BoundaryGeometry.parameter {q : OAI.CKSMetricGluing.SmoothMetric OAI.CKSBoundarySurface.I3 (M := N)} {k : OAI.CKSMetricGluing.InnerField OAI.CKSBoundarySurface.I3 (M := N)} (B : OAI.CKSMain.BoundaryGeometry q k) (p : OAI.CKSBoundarySurface.Boundary N) : OAI.CKSBoundarySurface.E2 → OAI.CKSBoundarySurface.E3 := (B.chart p).coordinate ∘ (Subtype.val : OAI.CKSBoundarySurface.Boundary N → N) ∘ (extChartAt OAI.CKSBoundarySurface.I2 p).symmdef BoundaryGeometry.thetaPlus {q : OAI.CKSMetricGluing.SmoothMetric OAI.CKSBoundarySurface.I3 (M := N)} {k : OAI.CKSMetricGluing.InnerField OAI.CKSBoundarySurface.I3 (M := N)} (B : OAI.CKSMain.BoundaryGeometry q k) (p : OAI.CKSBoundarySurface.Boundary N) : ℝ := let c := B.chart p let f := B.parameter p let y := (extChartAt OAI.CKSBoundarySurface.I2 p) p let ν := mfderiv OAI.CKSBoundarySurface.I3 𝓘(ℝ,OAI.CKSBoundarySurface.E3) c.coordinate p.val (B.normal p) OAI.CKSMain.meanCurvature c.metric f y ν + OAI.CKSMain.tangentialTrace c.metric c.tensor f ydef MarginalBoundary (q : OAI.CKSMetricGluing.SmoothMetric OAI.CKSBoundarySurface.I3 (M := N)) (k : OAI.CKSMetricGluing.InnerField OAI.CKSBoundarySurface.I3 (M := N)) : Prop := ∃ B : OAI.CKSMain.BoundaryGeometry q k, ∀ p, B.thetaPlus p = 0def bondiMass {g : OAI.CKSMetricGluing.SmoothMetric OAI.CKSBoundarySurface.I3 (M := N)} {K : OAI.CKSMetricGluing.InnerField OAI.CKSBoundarySurface.I3 (M := N)} (d : OAI.CKSSourceExterior.CKSData g K) : ℝ := Real.sqrt ((OAI.CKSLorentz.bondiCharge d.massAspect).1^2 - ‖(OAI.CKSLorentz.bondiCharge d.massAspect).2‖^2)end OAI.CKSMainendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSMainopen Set Filter Manifold Bundle CKSLorentz CKSMetricGluing CKSSpatialManifoldopen CKSBoundarySurface CKSIntrinsicConstraints CKSSourceExterioropen scoped ContDiff Topology InnerProductSpaceopen CKSSchwarzschildattribute [local instance] manifold_regularattribute [local instance] CKSIntrinsicConstraints.halfSpaceDimension_neZeroattribute [local instance] CKSSpatialManifold.real_id_isometric CKSLorentz.real_smulCommClass CKSLorentz.spatialDual_smulCommClasslocal instance atlas_manifold_one {N : Type u_1} [TopologicalSpace N] [ChartedSpace OAI.CKSBoundarySurface.H3 N] [IsManifold OAI.CKSBoundarySurface.I3 ∞ N] : IsManifold OAI.CKSBoundarySurface.I3 1 N := inferInstancelocal instance atlas_tangent_vectorBundle {N : Type u_1} [TopologicalSpace N] [ChartedSpace OAI.CKSBoundarySurface.H3 N] [IsManifold OAI.CKSBoundarySurface.I3 ∞ N] : letI := OAI.CKSMain.atlas_manifold_one (N := N) VectorBundle ℝ OAI.CKSBoundarySurface.E3 (fun x : N => TangentSpace OAI.CKSBoundarySurface.I3 x) := by infer_instanceabbrev CoefficientAtlas {N : Type u_1} [TopologicalSpace N] [ChartedSpace OAI.CKSBoundarySurface.H3 N] [IsManifold OAI.CKSBoundarySurface.I3 ∞ N] (q : OAI.CKSMetricGluing.SmoothMetric OAI.CKSBoundarySurface.I3 (M := N)) (k : OAI.CKSMetricGluing.InnerField OAI.CKSBoundarySurface.I3 (M := N)) := letI := OAI.CKSMain.atlas_manifold_one (N := N) letI := OAI.CKSMain.atlas_tangent_vectorBundle (N := N) let metric : ContMDiffRiemannianMetric OAI.CKSBoundarySurface.I3 ∞ OAI.CKSBoundarySurface.E3 (fun x : N => TangentSpace OAI.CKSBoundarySurface.I3 x) := q ∀ x : N, OAI.CKSIntrinsicConstraints.ConstraintChart metric.inner k xend OAI.CKSMainendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSMainopen Set Filter Manifold Bundle CKSLorentz CKSMetricGluing CKSSpatialManifoldopen CKSBoundarySurface CKSIntrinsicConstraints CKSSourceExterioropen scoped ContDiff Topologyattribute [local instance] manifold_regularvariable {N : Type u} [TopologicalSpace N] [ChartedSpace H3 N] [IsManifold I3 ∞ N]structure InteriorSurface (q : OAI.CKSMetricGluing.SmoothMetric OAI.CKSBoundarySurface.I3 (M := N)) (k : OAI.CKSMetricGluing.InnerField OAI.CKSBoundarySurface.I3 (M := N)) (A : OAI.CKSMain.CoefficientAtlas q k) (T : Type v) [TopologicalSpace T] [ChartedSpace OAI.CKSBoundarySurface.E2 T] [IsManifold OAI.CKSBoundarySurface.I2 ∞ T] where map : T → N smooth : ContMDiff OAI.CKSBoundarySurface.I2 OAI.CKSBoundarySurface.I3 ∞ map embedding : Topology.IsEmbedding map immersion : ∀ p, Function.Injective (mfderiv OAI.CKSBoundarySurface.I2 OAI.CKSBoundarySurface.I3 map p) interior : ∀ p, map p ∈ OAI.CKSBoundarySurface.I3.interior N normal : ∀ p, TangentSpace OAI.CKSBoundarySurface.I3 (map p) normal_unit : ∀ p, q.inner (map p) (normal p) (normal p) = 1 normal_orthogonal : ∀ p a, q.inner (map p) (normal p) (mfderiv OAI.CKSBoundarySurface.I2 OAI.CKSBoundarySurface.I3 map p a) = 0 normal_smooth : ∀ p, ContMDiffAt OAI.CKSBoundarySurface.I2 𝓘(ℝ,OAI.CKSBoundarySurface.E3) ∞ (fun t => mfderiv OAI.CKSBoundarySurface.I3 𝓘(ℝ,OAI.CKSBoundarySurface.E3) (A (map p)).coordinate (map t) (normal t)) pend OAI.CKSMainendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSMain.InteriorSurfaceopen Set Filter Manifold Bundle CKSLorentz CKSMetricGluing CKSSpatialManifoldopen CKSBoundarySurface CKSIntrinsicConstraints CKSSourceExterioropen scoped ContDiff Topologyattribute [local instance] manifold_regularvariable {N : Type u} [TopologicalSpace N] [ChartedSpace H3 N] [IsManifold I3 ∞ N]variable {q : SmoothMetric I3 (M := N)} {k : InnerField I3 (M := N)} {A : CoefficientAtlas q k} {T : Type v} [TopologicalSpace T] [ChartedSpace E2 T] [IsManifold I2 ∞ T] (D : InteriorSurface q k A T)def parameter (p : T) : OAI.CKSBoundarySurface.E2 → OAI.CKSBoundarySurface.E3 := (A (D.map p)).coordinate ∘ D.map ∘ (extChartAt OAI.CKSBoundarySurface.I2 p).symmdef mean (p : T) : ℝ := let c := A (D.map p) OAI.CKSMain.meanCurvature c.metric (D.parameter p) ((extChartAt OAI.CKSBoundarySurface.I2 p) p) (mfderiv OAI.CKSBoundarySurface.I3 𝓘(ℝ,OAI.CKSBoundarySurface.E3) c.coordinate (D.map p) (D.normal p))def trace (p : T) : ℝ := let c := A (D.map p) OAI.CKSMain.tangentialTrace c.metric c.tensor (D.parameter p) ((extChartAt OAI.CKSBoundarySurface.I2 p) p)def thetaPlus (p : T) : ℝ := D.mean p + D.trace pdef thetaMinus (p : T) : ℝ := D.mean p - D.trace pdef SeparatesAway (c : OAI.CKSSourceExterior.CoordinateEnd (N := N)) : Prop := ∃ B : Set N, B = closure (_root_.interior B) ∧ (_root_.interior B).Nonempty ∧ frontier B = range D.map ∧ ∃ r : ℝ, c.radius < r ∧ B ⊆ {x | x ∉ c.domain ∨ ‖c.coordinate x‖ ≤ r}def ComponentwiseApparent : Prop := ∀ p : T, (∀ z ∈ connectedComponent p, D.thetaPlus z = 0) ∨ (∀ z ∈ connectedComponent p, D.thetaMinus z = 0)end OAI.CKSMain.InteriorSurfaceendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSMainopen Set Filter Manifold Bundle CKSLorentz CKSMetricGluing CKSSpatialManifoldopen CKSBoundarySurface CKSIntrinsicConstraints CKSSourceExterioropen scoped ContDiff Topologyattribute [local instance] manifold_regularvariable {N : Type u} [TopologicalSpace N] [ChartedSpace H3 N] [IsManifold I3 ∞ N]def NoAdditionalHorizons (q : OAI.CKSMetricGluing.SmoothMetric OAI.CKSBoundarySurface.I3 (M := N)) (k : OAI.CKSMetricGluing.InnerField OAI.CKSBoundarySurface.I3 (M := N)) (c : OAI.CKSSourceExterior.CoordinateEnd (N := N)) (A : OAI.CKSMain.CoefficientAtlas q k) : Prop := ∀ (T : Type v) [TopologicalSpace T] [ChartedSpace OAI.CKSBoundarySurface.E2 T] [IsManifold OAI.CKSBoundarySurface.I2 ∞ T] [T2Space T] [SecondCountableTopology T] [CompactSpace T] [Nonempty T] (D : OAI.CKSMain.InteriorSurface q k A T), D.SeparatesAway c → ¬ D.ComponentwiseApparentstructure MainHypotheses [T2Space N] [SecondCountableTopology N] [ConnectedSpace N] (g : OAI.CKSMetricGluing.SmoothMetric OAI.CKSBoundarySurface.I3 (M := N)) (K : OAI.CKSMetricGluing.InnerField OAI.CKSBoundarySurface.I3 (M := N)) (d : OAI.CKSSourceExterior.CKSData g K) (A : OAI.CKSMain.CoefficientAtlas g K) : Prop where smooth_tensor : ContMDiff OAI.CKSBoundarySurface.I3 (OAI.CKSBoundarySurface.I3.prod 𝓘(ℝ,OAI.CKSLorentz.SpatialBilinear)) ∞ (OAI.CKSMetricGluing.innerSection OAI.CKSBoundarySurface.I3 K) symmetric_tensor : ∀ x v w, K x v w = K x w v orientable : OAI.CKSSourceExterior.Orientable (N := N) boundary_compact : IsCompact (OAI.CKSBoundarySurface.I3.boundary N) boundary_nonempty : (OAI.CKSBoundarySurface.I3.boundary N).Nonempty complete : OAI.CKSReplacementCompleteness.IsComplete OAI.CKSBoundarySurface.I3 g.toContinuousRiemannianMetric dec : OAI.CKSSpatialManifold.PhysicalDEC OAI.CKSBoundarySurface.I3 g.inner K timelike : ‖(OAI.CKSLorentz.bondiCharge d.massAspect).2‖ < (OAI.CKSLorentz.bondiCharge d.massAspect).1 boundary_connected : ConnectedSpace (OAI.CKSBoundarySurface.Boundary N) boundary_marginal : OAI.CKSMain.MarginalBoundary g K positive_area : 0 < OAI.CKSSourceExterior.minimumEnclosingArea g no_horizons : OAI.CKSMain.NoAdditionalHorizons.{u,v} g K d.chart Aend OAI.CKSMainendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSMainopen Set Filter Manifold Bundle CKSLorentz CKSMetricGluing CKSSpatialManifoldopen CKSBoundarySurface CKSIntrinsicConstraints CKSSourceExterioropen scoped ContDiff Topologyattribute [local instance] manifold_regularvariable {N : Type u} [TopologicalSpace N] [ChartedSpace H3 N] [IsManifold I3 ∞ N]attribute [local instance] sixteen_atLeastTwodef SchwarzschildExample (m : ℝ) (_hm : 0 < m) : Prop := ∃ (g : OAI.CKSMetricGluing.SmoothMetric OAI.CKSBoundarySurface.I3 (M := OAI.CKSSchwarzschild.Exterior)) (d : OAI.CKSSourceExterior.CKSData g (OAI.CKSSchwarzschild.tensorInner m)) (A : OAI.CKSMain.CoefficientAtlas g (OAI.CKSSchwarzschild.tensorInner m)), (∀ p, g.inner p = OAI.CKSSchwarzschild.metricInner m p) ∧ OAI.CKSMain.MainHypotheses.{0,v} g (OAI.CKSSchwarzschild.tensorInner m) d A ∧ OAI.CKSSchwarzschild.HorizonRegularGraph m ∧ OAI.CKSMain.bondiMass d = m ∧ OAI.CKSSourceExterior.minimumEnclosingArea g = 16*Real.pi*m^2 ∧ OAI.CKSMain.bondiMass d = Real.sqrt (OAI.CKSSourceExterior.minimumEnclosingArea g / (16*Real.pi))end OAI.CKSMainendnoncomputable sectionuniverse u v w u_1 u_2 u_3 u_4 u_5 u_6namespace OAI.CKSMainopen Set Filter Manifold Bundle CKSLorentz CKSMetricGluing CKSSpatialManifoldopen CKSBoundarySurface CKSIntrinsicConstraints CKSSourceExterioropen scoped ContDiff Topologyattribute [local instance] manifold_regularopen CKSSchwarzschildtheorem schwarzschild_equality_examples (m : ℝ) (hm : 0 < m) : SchwarzschildExample.{v} m hm := by sorryend OAI.CKSMainend