Link with the local story

This file bridges the gap between Chapter 2 and Chapter 3. It builds on SmoothEmbedding.lean but goes all the way to vector spaces (the previous file is about embedding any manifold into another one).

Localizing relations and 1-jet sections

Now we really bridge the gap all the way to vector spaces.

def OneJetSec.loc {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {E' : Type u_2} [NormedAddCommGroup E'] [NormedSpace ℝ E'] (F : OneJetSec (modelWithCornersSelf ℝ E) E (modelWithCornersSelf ℝ E') E') : JetSec E E'

Convert a 1-jet section between vector spaces seen as manifold to a 1-jet section between those vector spaces.

Equations

• F.loc = { f := F.bs, f_diff := ⋯, φ := fun (x : E) => (F x).snd, φ_diff := ⋯ }

theorem OneJetSec.loc_hol_at_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {E' : Type u_2} [NormedAddCommGroup E'] [NormedSpace ℝ E'] (F : OneJetSec (modelWithCornersSelf ℝ E) E (modelWithCornersSelf ℝ E') E') (x : E) : F.loc.IsHolonomicAt x ↔ F.IsHolonomicAt x

def RelMfld.relLoc {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {E' : Type u_2} [NormedAddCommGroup E'] [NormedSpace ℝ E'] (R : RelMfld (modelWithCornersSelf ℝ E) E (modelWithCornersSelf ℝ E') E') : RelLoc E E'

Turns a relation between E and E' seen as manifolds into a relation between them seen as vector spaces. One annoying bit is equiv.prod_assoc E E' (E →L[ℝ] E') that is needed to reassociate a product of types.

Equations

• R.relLoc = ⇑(Homeomorph.prodAssoc E E' (E →L[ℝ] E')).symm ⁻¹' (⇑(oneJetBundleModelSpaceHomeomorph (modelWithCornersSelf ℝ E) (modelWithCornersSelf ℝ E')).symm ⁻¹' R)

theorem ample_of_ample {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {E' : Type u_2} [NormedAddCommGroup E'] [NormedSpace ℝ E'] (R : RelMfld (modelWithCornersSelf ℝ E) E (modelWithCornersSelf ℝ E') E') (hR : R.Ample) : R.relLoc.IsAmple

theorem isOpen_of_isOpen {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {E' : Type u_2} [NormedAddCommGroup E'] [NormedSpace ℝ E'] (R : RelMfld (modelWithCornersSelf ℝ E) E (modelWithCornersSelf ℝ E') E') (hR : IsOpen R) : IsOpen R.relLoc

Unlocalizing relations and 1-jet sections

def JetSec.unloc {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {E' : Type u_2} [NormedAddCommGroup E'] [NormedSpace ℝ E'] (𝓕 : JetSec E E') : OneJetSec (modelWithCornersSelf ℝ E) E (modelWithCornersSelf ℝ E') E'

Convert a 1-jet section between vector spaces to a 1-jet section between those vector spaces seen as manifolds.

Equations

• 𝓕.unloc = { bs := 𝓕.f, ϕ := fun (x : E) => (𝓕 x).2, smooth' := ⋯ }

theorem JetSec.unloc_hol_at_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {E' : Type u_2} [NormedAddCommGroup E'] [NormedSpace ℝ E'] (𝓕 : JetSec E E') (x : E) : 𝓕.unloc.IsHolonomicAt x ↔ 𝓕.IsHolonomicAt x

def HtpyJetSec.unloc {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {E' : Type u_2} [NormedAddCommGroup E'] [NormedSpace ℝ E'] (𝓕 : HtpyJetSec E E') : HtpyOneJetSec (modelWithCornersSelf ℝ E) E (modelWithCornersSelf ℝ E') E'

Equations

• 𝓕.unloc = { bs := fun (t : ℝ) => (𝓕 t).f, ϕ := fun (t : ℝ) (x : E) => ((𝓕 t) x).2, smooth' := ⋯ }

structure ChartPair {E : Type u₁} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u₂} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) (M : Type u₃) [TopologicalSpace M] [ChartedSpace H M] {E' : Type u₄} [NormedAddCommGroup E'] [NormedSpace ℝ E'] {H' : Type u₅} [TopologicalSpace H'] (I' : ModelWithCorners ℝ E' H') (M' : Type u₆) [MetricSpace M'] [ChartedSpace H' M'] : Type (max (max (max u₁ u₃) u₄) u₆)

A pair of charts together with a compact subset of the first vector space.

• φ : OpenSmoothEmbedding (modelWithCornersSelf ℝ E) E I M
• ψ : OpenSmoothEmbedding (modelWithCornersSelf ℝ E') E' I' M'
• K₁ : Set E
• hK₁ : IsCompact self.K₁

def FormalSol.localize {E : Type u₁} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u₂} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u₃} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] {E' : Type u₄} [NormedAddCommGroup E'] [NormedSpace ℝ E'] {H' : Type u₅} [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} {M' : Type u₆} [MetricSpace M'] [ChartedSpace H' M'] [IsManifold I' (↑⊤) M'] {R : RelMfld I M I' M'} (p : ChartPair I M I' M') (F : FormalSol R) (hF : Set.range (F.bs ∘ ↑p.φ) ⊆ Set.range ↑p.ψ) : (RelMfld.localize p.φ p.ψ R).relLoc.FormalSol

Equations

• FormalSol.localize p F hF = { toJetSec := (F.localize p.φ p.ψ hF).loc, is_sol := ⋯ }

theorem FormalSol.isHolonomicLocalize {E : Type u₁} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u₂} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u₃} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] {E' : Type u₄} [NormedAddCommGroup E'] [NormedSpace ℝ E'] {H' : Type u₅} [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} {M' : Type u₆} [MetricSpace M'] [ChartedSpace H' M'] [IsManifold I' (↑⊤) M'] {R : RelMfld I M I' M'} (p : ChartPair I M I' M') (F : FormalSol R) (hF : Set.range (F.bs ∘ ↑p.φ) ⊆ Set.range ↑p.ψ) (x : E) (hx : F.IsHolonomicAt (↑p.φ x)) : (localize p F hF).IsHolonomicAt x

structure ChartPair.compat' {E : Type u₁} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u₂} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u₃} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] {E' : Type u₄} [NormedAddCommGroup E'] [NormedSpace ℝ E'] {H' : Type u₅} [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} {M' : Type u₆} [MetricSpace M'] [ChartedSpace H' M'] [IsManifold I' (↑⊤) M'] {R : RelMfld I M I' M'} (p : ChartPair I M I' M') (F : FormalSol R) (𝓕 : (RelMfld.localize p.φ p.ψ R).relLoc.HtpyFormalSol) : Prop

• hF : Set.range (F.bs ∘ ↑p.φ) ⊆ Set.range ↑p.ψ
• hFF (x : E) : x ∉ p.K₁ → ∀ (t : ℝ), (𝓕 t) x = (FormalSol.localize p F ⋯) x

def RelLoc.HtpyFormalSol.unloc {E : Type u₁} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u₂} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u₃} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u₄} [NormedAddCommGroup E'] [NormedSpace ℝ E'] {H' : Type u₅} [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} {M' : Type u₆} [MetricSpace M'] [ChartedSpace H' M'] {R : RelMfld I M I' M'} (p : ChartPair I M I' M') (𝓕 : (RelMfld.localize p.φ p.ψ R).relLoc.HtpyFormalSol) : _root_.HtpyFormalSol (RelMfld.localize p.φ p.ψ R)

Equations

• RelLoc.HtpyFormalSol.unloc p 𝓕 = { toFamilyOneJetSec := 𝓕.toHtpyJetSec.unloc, is_sol' := ⋯ }

theorem RelLoc.HtpyFormalSol.unloc_congr {E : Type u₁} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u₂} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u₃} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u₄} [NormedAddCommGroup E'] [NormedSpace ℝ E'] {H' : Type u₅} [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} {M' : Type u₆} [MetricSpace M'] [ChartedSpace H' M'] {R : RelMfld I M I' M'} (p : ChartPair I M I' M') {𝓕 𝓕' : (RelMfld.localize p.φ p.ψ R).relLoc.HtpyFormalSol} {t t' : ℝ} {x : E} (h : (𝓕 t) x = (𝓕' t') x) : ((unloc p 𝓕) t) x = ((unloc p 𝓕') t') x

theorem RelLoc.HtpyFormalSol.unloc_congr_const {E : Type u₁} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u₂} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u₃} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u₄} [NormedAddCommGroup E'] [NormedSpace ℝ E'] {H' : Type u₅} [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} {M' : Type u₆} [MetricSpace M'] [ChartedSpace H' M'] {R : RelMfld I M I' M'} (p : ChartPair I M I' M') {𝓕 : (RelMfld.localize p.φ p.ψ R).relLoc.HtpyFormalSol} {𝓕' : (RelMfld.localize p.φ p.ψ R).relLoc.FormalSol} {t : ℝ} {x : E} (h : (𝓕 t) x = 𝓕' x) : ((unloc p 𝓕) t) x = (↑𝓕').unloc x

theorem RelLoc.HtpyFormalSol.unloc_congr' {E : Type u₁} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u₂} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u₃} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u₄} [NormedAddCommGroup E'] [NormedSpace ℝ E'] {H' : Type u₅} [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} {M' : Type u₆} [MetricSpace M'] [ChartedSpace H' M'] {R : RelMfld I M I' M'} (p : ChartPair I M I' M') {𝓕 𝓕' : (RelMfld.localize p.φ p.ψ R).relLoc.HtpyFormalSol} {t t' : ℝ} (h : 𝓕 t = 𝓕' t') : (unloc p 𝓕) t = (unloc p 𝓕') t'

@[simp]

theorem FormalSol.transfer_unloc_localize {E : Type u₁} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u₂} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u₃} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] {E' : Type u₄} [NormedAddCommGroup E'] [NormedSpace ℝ E'] {H' : Type u₅} [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} {M' : Type u₆} [MetricSpace M'] [ChartedSpace H' M'] [IsManifold I' (↑⊤) M'] {R : RelMfld I M I' M'} (p : ChartPair I M I' M') (F : FormalSol R) (hF : Set.range (F.bs ∘ ↑p.φ) ⊆ Set.range ↑p.ψ) (x : E) : p.φ.transfer p.ψ ((↑(localize p F hF)).unloc x) = F (↑p.φ x)

theorem ChartPair.mkHtpy_aux {E : Type u₁} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u₂} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u₃} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] {E' : Type u₄} [NormedAddCommGroup E'] [NormedSpace ℝ E'] {H' : Type u₅} [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} {M' : Type u₆} [MetricSpace M'] [ChartedSpace H' M'] [IsManifold I' (↑⊤) M'] {R : RelMfld I M I' M'} (p : ChartPair I M I' M') {F : FormalSol R} {𝓕 : (RelMfld.localize p.φ p.ψ R).relLoc.HtpyFormalSol} (h : p.compat' F 𝓕) (t : ℝ) (x : E) (hx : x ∉ p.K₁) : F (↑p.φ x) = ↑(OneJetBundle.embedding p.φ p.ψ) (((RelLoc.HtpyFormalSol.unloc p 𝓕) t) x)

def ChartPair.mkHtpy {E : Type u₁} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u₂} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u₃} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] {E' : Type u₄} [NormedAddCommGroup E'] [NormedSpace ℝ E'] {H' : Type u₅} [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} {M' : Type u₆} [MetricSpace M'] [ChartedSpace H' M'] [IsManifold I' (↑⊤) M'] {R : RelMfld I M I' M'} (p : ChartPair I M I' M') [T2Space M] (F : FormalSol R) (𝓕 : (RelMfld.localize p.φ p.ψ R).relLoc.HtpyFormalSol) : HtpyFormalSol R

Equations

• p.mkHtpy F 𝓕 = if h : p.compat' F 𝓕 then p.φ.updateFormalSol p.ψ F (RelLoc.HtpyFormalSol.unloc p 𝓕) ⋯ ⋯ else F.constHtpy

theorem ChartPair.mkHtpy_congr {E : Type u₁} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u₂} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u₃} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] {E' : Type u₄} [NormedAddCommGroup E'] [NormedSpace ℝ E'] {H' : Type u₅} [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} {M' : Type u₆} [MetricSpace M'] [ChartedSpace H' M'] [IsManifold I' (↑⊤) M'] {R : RelMfld I M I' M'} (p : ChartPair I M I' M') [T2Space M] (F : FormalSol R) {𝓕 : (RelMfld.localize p.φ p.ψ R).relLoc.HtpyFormalSol} {t t' : ℝ} (h : 𝓕 t = 𝓕 t') : (p.mkHtpy F 𝓕) t = (p.mkHtpy F 𝓕) t'

theorem ChartPair.mkHtpy_eq_self {E : Type u₁} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u₂} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u₃} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] {E' : Type u₄} [NormedAddCommGroup E'] [NormedSpace ℝ E'] {H' : Type u₅} [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} {M' : Type u₆} [MetricSpace M'] [ChartedSpace H' M'] [IsManifold I' (↑⊤) M'] {R : RelMfld I M I' M'} (p : ChartPair I M I' M') [T2Space M] (F : FormalSol R) (𝓕 : (RelMfld.localize p.φ p.ψ R).relLoc.HtpyFormalSol) {t : ℝ} {m : M} (hm : ∀ (hF : Set.range (F.bs ∘ ↑p.φ) ⊆ Set.range ↑p.ψ), ∀ x ∈ p.K₁, m = ↑p.φ x → (𝓕 t) x = (FormalSol.localize p F hF) x) : ((p.mkHtpy F 𝓕) t) m = F m

theorem ChartPair.mkHtpy_eq_of_not_mem {E : Type u₁} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u₂} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u₃} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] {E' : Type u₄} [NormedAddCommGroup E'] [NormedSpace ℝ E'] {H' : Type u₅} [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} {M' : Type u₆} [MetricSpace M'] [ChartedSpace H' M'] [IsManifold I' (↑⊤) M'] {R : RelMfld I M I' M'} (p : ChartPair I M I' M') [T2Space M] (F : FormalSol R) (𝓕 : (RelMfld.localize p.φ p.ψ R).relLoc.HtpyFormalSol) {t : ℝ} {m : M} (hm : m ∉ ↑p.φ '' p.K₁) : ((p.mkHtpy F 𝓕) t) m = F m

theorem ChartPair.mkHtpy_eq_of_eq {E : Type u₁} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u₂} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u₃} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] {E' : Type u₄} [NormedAddCommGroup E'] [NormedSpace ℝ E'] {H' : Type u₅} [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} {M' : Type u₆} [MetricSpace M'] [ChartedSpace H' M'] [IsManifold I' (↑⊤) M'] {R : RelMfld I M I' M'} (p : ChartPair I M I' M') [T2Space M] (F : FormalSol R) (𝓕 : (RelMfld.localize p.φ p.ψ R).relLoc.HtpyFormalSol) (h𝓕 : p.compat' F 𝓕) {t : ℝ} {x : E} (h : (𝓕 t) x = (FormalSol.localize p F ⋯) x) : ((p.mkHtpy F 𝓕) t) (↑p.φ x) = F (↑p.φ x)

theorem ChartPair.mkHtpy_eq_of_forall {E : Type u₁} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u₂} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u₃} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] {E' : Type u₄} [NormedAddCommGroup E'] [NormedSpace ℝ E'] {H' : Type u₅} [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} {M' : Type u₆} [MetricSpace M'] [ChartedSpace H' M'] [IsManifold I' (↑⊤) M'] {R : RelMfld I M I' M'} (p : ChartPair I M I' M') [T2Space M] {F : FormalSol R} {𝓕 : (RelMfld.localize p.φ p.ψ R).relLoc.HtpyFormalSol} (h𝓕 : p.compat' F 𝓕) {t : ℝ} (h : 𝓕 t = ↑(FormalSol.localize p F ⋯)) : (p.mkHtpy F 𝓕) t = F

theorem ChartPair.mkHtpy_localize {E : Type u₁} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u₂} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u₃} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] {E' : Type u₄} [NormedAddCommGroup E'] [NormedSpace ℝ E'] {H' : Type u₅} [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} {M' : Type u₆} [MetricSpace M'] [ChartedSpace H' M'] [IsManifold I' (↑⊤) M'] {R : RelMfld I M I' M'} (p : ChartPair I M I' M') [T2Space M] {F : FormalSol R} {𝓕 : (RelMfld.localize p.φ p.ψ R).relLoc.HtpyFormalSol} {t : ℝ} {e : E} (h : p.compat' F 𝓕) (rg : Set.range (((p.mkHtpy F 𝓕) t).bs ∘ ↑p.φ) ⊆ Set.range ↑p.ψ) : (((p.mkHtpy F 𝓕) t).localize p.φ p.ψ rg) e = (𝓕 t).unloc e

theorem ChartPair.mkHtpy_isHolonomicAt_iff {E : Type u₁} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u₂} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u₃} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] {E' : Type u₄} [NormedAddCommGroup E'] [NormedSpace ℝ E'] {H' : Type u₅} [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} {M' : Type u₆} [MetricSpace M'] [ChartedSpace H' M'] [IsManifold I' (↑⊤) M'] {R : RelMfld I M I' M'} (p : ChartPair I M I' M') [T2Space M] {F : FormalSol R} {𝓕 : (RelMfld.localize p.φ p.ψ R).relLoc.HtpyFormalSol} (h : p.compat' F 𝓕) {t : ℝ} {e : E} : ((p.mkHtpy F 𝓕) t).IsHolonomicAt (↑p.φ e) ↔ (𝓕 t).IsHolonomicAt e

theorem ChartPair.dist_update' {E : Type u₁} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u₂} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u₃} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] {E' : Type u₄} [NormedAddCommGroup E'] [NormedSpace ℝ E'] {H' : Type u₅} [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} {M' : Type u₆} [MetricSpace M'] [ChartedSpace H' M'] [IsManifold I' (↑⊤) M'] {R : RelMfld I M I' M'} (p : ChartPair I M I' M') [T2Space M] [FiniteDimensional ℝ E'] {δ : M → ℝ} (hδ_pos : ∀ (x : M), 0 < δ x) (hδ_cont : Continuous δ) {F : FormalSol R} (hF : Set.range (F.bs ∘ ↑p.φ) ⊆ Set.range ↑p.ψ) : ∃ η > 0, ∀ {𝓕 : (RelMfld.localize p.φ p.ψ R).relLoc.HtpyFormalSol}, p.compat' F 𝓕 → ∀ e ∈ p.K₁, ∀ t ∈ Set.Icc 0 1, ‖(𝓕 t).f e - (↑(FormalSol.localize p F hF)).f e‖ < η → dist (((p.mkHtpy F 𝓕) t).bs (↑p.φ e)) (F.bs (↑p.φ e)) < δ (↑p.φ e)