LeanPool.SardMoreira.Chart #

source

theorem fderiv_comp_prodMk {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : E × F → G} {a : E} {b : F} (hdf : DifferentiableAt 𝕜 f (a, b)) :

fderiv 𝕜 (fun (y : F) => f (a, y)) b = fderiv 𝕜 f (a, b) ∘SL ContinuousLinearMap.inr 𝕜 E F

source

theorem fderiv_comp_prodMk' {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : E × F → G} {a : E × F} (hdf : DifferentiableAt 𝕜 f a) :

fderiv 𝕜 (fun (y : F) => f (a.1, y)) a.2 = fderiv 𝕜 f a ∘SL ContinuousLinearMap.inr 𝕜 E F

source

theorem fderiv_curry {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : E × F → G} {a : E} {b : F} (hdf : DifferentiableAt 𝕜 f (a, b)) :

fderiv 𝕜 (Function.curry f a) b = fderiv 𝕜 f (a, b) ∘SL ContinuousLinearMap.inr 𝕜 E F

source

@[irreducible]

noncomputable def Moreira2001.chartImplicitData {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {k : ℕ} {α : ↑unitInterval} (f : E × F → ℝ) (a : E × F) (hfa : ContDiffMoreiraHolderAt k α f a) (hk : k ≠ 0) (hdf : fderiv ℝ f a ∘SL ContinuousLinearMap.inr ℝ E F ≠ 0) :

ImplicitFunctionData ℝ (E × F) ℝ (E × ↥(↑(fderiv ℝ f a ∘SL ContinuousLinearMap.inr ℝ E F)).ker)

Implicit-function data used to build a local Moreira chart at a non-large point.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem Moreira2001.chartImplicitData_leftFun {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {k : ℕ} {α : ↑unitInterval} {f : E × F → ℝ} {a : E × F} (hfa : ContDiffMoreiraHolderAt k α f a) (hk : k ≠ 0) (hdf : fderiv ℝ f a ∘SL ContinuousLinearMap.inr ℝ E F ≠ 0) :

(chartImplicitData f a hfa hk hdf).leftFun = f

source

@[simp]

theorem Moreira2001.chartImplicitData_leftDeriv {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {k : ℕ} {α : ↑unitInterval} {f : E × F → ℝ} {a : E × F} (hfa : ContDiffMoreiraHolderAt k α f a) (hk : k ≠ 0) (hdf : fderiv ℝ f a ∘SL ContinuousLinearMap.inr ℝ E F ≠ 0) :

(chartImplicitData f a hfa hk hdf).leftDeriv = fderiv ℝ f a

source

@[simp]

theorem Moreira2001.fst_rightFun_chartImplicitData {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {k : ℕ} {α : ↑unitInterval} {f : E × F → ℝ} {a : E × F} (hfa : ContDiffMoreiraHolderAt k α f a) (hk : k ≠ 0) (hdf : fderiv ℝ f a ∘SL ContinuousLinearMap.inr ℝ E F ≠ 0) (x : E × F) :

((chartImplicitData f a hfa hk hdf).rightFun x).1 = x.1

source

@[simp]

theorem Moreira2001.chartImplicitData_pt {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {k : ℕ} {α : ↑unitInterval} {f : E × F → ℝ} {a : E × F} (hfa : ContDiffMoreiraHolderAt k α f a) (hk : k ≠ 0) (hdf : fderiv ℝ f a ∘SL ContinuousLinearMap.inr ℝ E F ≠ 0) :

(chartImplicitData f a hfa hk hdf).pt = a

source

theorem Moreira2001.chartImplicitData_rightDeriv_apply_ker {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {k : ℕ} {α : ↑unitInterval} {f : E × F → ℝ} {a : E × F} (hfa : ContDiffMoreiraHolderAt k α f a) (hk : k ≠ 0) (hdf : fderiv ℝ f a ∘SL ContinuousLinearMap.inr ℝ E F ≠ 0) (x : E) {y : F} (hy : (fderiv ℝ f a) (0, y) = 0) :

(chartImplicitData f a hfa hk hdf).rightDeriv (x, y) = (x, ⟨y, ⋯⟩)

source

theorem Moreira2001.fderiv_implicitFunction_chartImplicitData_apply_mk_zero {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {k : ℕ} {α : ↑unitInterval} {f : E × F → ℝ} {a : E × F} (hfa : ContDiffMoreiraHolderAt k α f a) (hk : k ≠ 0) (hdf : fderiv ℝ f a ∘SL ContinuousLinearMap.inr ℝ E F ≠ 0) (y : ↥(↑(fderiv ℝ f a ∘SL ContinuousLinearMap.inr ℝ E F)).ker) :

(fderiv ℝ ((chartImplicitData f a hfa hk hdf).implicitFunction (f a)) ((chartImplicitData f a hfa hk hdf).rightFun a)) (0, y) = (0, ↑y)

source

theorem Moreira2001.fderiv_implicitFunction_chartImplicitData_comp_inr {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {k : ℕ} {α : ↑unitInterval} {f : E × F → ℝ} {a : E × F} (hfa : ContDiffMoreiraHolderAt k α f a) (hk : k ≠ 0) (hdf : fderiv ℝ f a ∘SL ContinuousLinearMap.inr ℝ E F ≠ 0) :

fderiv ℝ ((chartImplicitData f a hfa hk hdf).implicitFunction (f a)) ((chartImplicitData f a hfa hk hdf).rightFun a) ∘SL ContinuousLinearMap.inr ℝ E ↥(↑(fderiv ℝ f a ∘SL ContinuousLinearMap.inr ℝ E F)).ker = ContinuousLinearMap.inr ℝ E F ∘SL (↑(fderiv ℝ f a ∘SL ContinuousLinearMap.inr ℝ E F)).ker.subtypeL

source

theorem Moreira2001.fst_implicitFunction_chartImplicitDataEventuallyEq {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {k : ℕ} {α : ↑unitInterval} {f : E × F → ℝ} {a : E × F} (hfa : ContDiffMoreiraHolderAt k α f a) (hk : k ≠ 0) (hdf : fderiv ℝ f a ∘SL ContinuousLinearMap.inr ℝ E F ≠ 0) :

Prod.fst ∘ (chartImplicitData f a hfa hk hdf).implicitFunction (f a) =ᶠ[nhds ((chartImplicitData f a hfa hk hdf).rightFun a)] Prod.fst

source

theorem Moreira2001.map_implicitFunction_chartImplicitData_nhdsWithin_preimage {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {k : ℕ} {α : ↑unitInterval} {f : E × F → ℝ} {a : E × F} (hfa : ContDiffMoreiraHolderAt k α f a) (hk : k ≠ 0) (hdf : fderiv ℝ f a ∘SL ContinuousLinearMap.inr ℝ E F ≠ 0) (s : Set (E × F)) (hfs : f =ᶠ[nhdsWithin a s] 0) (ha : a ∈ s) :

Filter.map ((chartImplicitData f a hfa hk hdf).implicitFunction 0) (nhdsWithin ((chartImplicitData f a hfa hk hdf).rightFun a) ((chartImplicitData f a hfa hk hdf).implicitFunction 0 ⁻¹' s)) = nhdsWithin a s

source

def Moreira2001.IsLargeAt {E : Type u} {G : Type w} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup G] [NormedSpace ℝ G] (k : ℕ) (α : ↑unitInterval) (s : Set (E × G)) (a : E × G) :

Prop

The local largeness condition used in Moreira's recursive covering argument.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem Moreira2001.IsLargeAt.fderiv_comp_inr_eq_zero {E : Type u} {F : Type v} {G : Type w} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {k : ℕ} {α : ↑unitInterval} {s : Set (E × F)} {a : E × F} (h : IsLargeAt k α s a) {f : E × F → G} (hf : ∀ᶠ (x : E × F) in nhdsWithin a s, ContDiffMoreiraHolderAt k α f x) (hf₀ : f =ᶠ[nhdsWithin a s] 0) :

fderiv ℝ f a ∘SL ContinuousLinearMap.inr ℝ E F = 0

Definition of IsLargeAt talks about f : E × F → ℝ only, but it implies a similar statement for any codomain.

source

structure Moreira2001.Chart {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (k : ℕ) (α : ↑unitInterval) (s : Set (E × F)) :

Type (max u (v + 1))

A Moreira chart of depth k covering part of a set in a product space.

Dom : Type v
The second-coordinate domain of the chart.
instNormedAddCommGroupDom : NormedAddCommGroup self.Dom
instNormedSpaceDom : NormedSpace ℝ self.Dom
instFiniteDimensional : FiniteDimensional ℝ self.Dom
toFun : E × self.Dom → E × F
The chart map into the original product space.
set : Set (E × self.Dom)
The part of the chart domain covered by this chart.
fst_apply (x : E × self.Dom) : (↑self x).1 = x.1
contDiffMoreiraHolderAt {x : E × self.Dom} : x ∈ self.set → ContDiffMoreiraHolderAt k α (↑self) x
injective_fderiv {x : E × self.Dom} : x ∈ self.set → Function.Injective ⇑(fderiv ℝ (↑self) x)
finrank_le : Module.finrank ℝ self.Dom ≤ Module.finrank ℝ F
mapsTo : Set.MapsTo (↑self) self.set s

Instances For

source

@[implicit_reducible]

instance Moreira2001.Chart.instCoeFunForallProdDom {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} {α : ↑unitInterval} {s : Set (E × F)} :

CoeFun (Chart k α s) fun (ψ : Chart k α s) => E × ψ.Dom → E × F

Equations

Moreira2001.Chart.instCoeFunForallProdDom = { coe := Moreira2001.Chart.toFun }

source

@[simp]

theorem Moreira2001.Chart.prodMk_fst_snd_apply {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} {α : ↑unitInterval} {s : Set (E × F)} (φ : Chart k α s) (x : E × φ.Dom) :

(x.1, (↑φ x).2) = ↑φ x

source

@[simp]

theorem Moreira2001.Chart.prodMk_snd_apply_mk {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} {α : ↑unitInterval} {s : Set (E × F)} (φ : Chart k α s) (x : E) (y : φ.Dom) :

(x, (↑φ (x, y)).2) = ↑φ (x, y)

source

theorem Moreira2001.Chart.continuousAt {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} {α : ↑unitInterval} {s : Set (E × F)} (f : Chart k α s) {x : E × f.Dom} (hx : x ∈ f.set) :

ContinuousAt (↑f) x

source

theorem Moreira2001.Chart.contDiffAt {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} {α : ↑unitInterval} {s : Set (E × F)} (f : Chart k α s) {x : E × f.Dom} (hx : x ∈ f.set) :

ContDiffAt ℝ (↑k) (↑f) x

source

theorem Moreira2001.Chart.eventually_differentiableAt {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} {α : ↑unitInterval} {s : Set (E × F)} (f : Chart k α s) {x : E × f.Dom} (hx : x ∈ f.set) (hk : k ≠ 0) :

∀ᶠ (y : E × f.Dom) in nhds x, DifferentiableAt ℝ (↑f) y

source

theorem Moreira2001.Chart.differentiableAt {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} {α : ↑unitInterval} {s : Set (E × F)} (f : Chart k α s) (hk : k ≠ 0) {x : E × f.Dom} (hx : x ∈ f.set) :

DifferentiableAt ℝ (↑f) x

source

def Moreira2001.Chart.id {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {k : ℕ} {α : ↑unitInterval} {s : Set (E × F)} :

Chart k α s

The identity chart.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem Moreira2001.Chart.id_toFun {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {k : ℕ} {α : ↑unitInterval} {s : Set (E × F)} :

↑Chart.id = id

source

@[simp]

theorem Moreira2001.Chart.id_instNormedAddCommGroupDom {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {k : ℕ} {α : ↑unitInterval} {s : Set (E × F)} :

Chart.id.instNormedAddCommGroupDom = inst✝

source

@[simp]

theorem Moreira2001.Chart.id_Dom {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {k : ℕ} {α : ↑unitInterval} {s : Set (E × F)} :

Chart.id.Dom = F

source

@[simp]

theorem Moreira2001.Chart.id_instNormedSpaceDom {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {k : ℕ} {α : ↑unitInterval} {s : Set (E × F)} :

Chart.id.instNormedSpaceDom = inst✝

source

@[simp]

theorem Moreira2001.Chart.id_set {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {k : ℕ} {α : ↑unitInterval} {s : Set (E × F)} :

Chart.id.set = s

source

@[implicit_reducible]

instance Moreira2001.Chart.instInhabited {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {k : ℕ} {α : ↑unitInterval} {s : Set (E × F)} :

Inhabited (Chart k α s)

Equations

Moreira2001.Chart.instInhabited = { default := Moreira2001.Chart.id }

source

theorem Moreira2001.Chart.exists_dim_lt_map_nhdsWithin_eq {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {k : ℕ} {α : ↑unitInterval} {s : Set (E × F)} {a : E × F} (hs : ¬IsLargeAt k α s a) (hk : k ≠ 0) (has : a ∈ s) :

∃ (ψ : Chart k α s) (pt : E × ψ.Dom), Module.finrank ℝ ψ.Dom < Module.finrank ℝ F ∧ pt ∈ ψ.set ∧ Filter.map (↑ψ) (nhdsWithin pt ψ.set) = nhdsWithin a s

source

def Moreira2001.Chart.comp {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} {α : ↑unitInterval} {s : Set (E × F)} (g : Chart k α s) (f : Chart k α g.set) (hk : k ≠ 0) :

Chart k α s

Compose two charts of the same depth.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem Moreira2001.Chart.comp_set {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} {α : ↑unitInterval} {s : Set (E × F)} (g : Chart k α s) (f : Chart k α g.set) (hk : k ≠ 0) :

(g.comp f hk).set = f.set

source

@[simp]

theorem Moreira2001.Chart.comp_instNormedAddCommGroupDom {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} {α : ↑unitInterval} {s : Set (E × F)} (g : Chart k α s) (f : Chart k α g.set) (hk : k ≠ 0) :

(g.comp f hk).instNormedAddCommGroupDom = f.instNormedAddCommGroupDom

source

@[simp]

theorem Moreira2001.Chart.comp_toFun {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} {α : ↑unitInterval} {s : Set (E × F)} (g : Chart k α s) (f : Chart k α g.set) (hk : k ≠ 0) :

↑(g.comp f hk) = ↑g ∘ ↑f

source

@[simp]

theorem Moreira2001.Chart.comp_instNormedSpaceDom {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} {α : ↑unitInterval} {s : Set (E × F)} (g : Chart k α s) (f : Chart k α g.set) (hk : k ≠ 0) :

(g.comp f hk).instNormedSpaceDom = f.instNormedSpaceDom

source

@[simp]

theorem Moreira2001.Chart.comp_Dom {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} {α : ↑unitInterval} {s : Set (E × F)} (g : Chart k α s) (f : Chart k α g.set) (hk : k ≠ 0) :

(g.comp f hk).Dom = f.Dom

source

def Moreira2001.Chart.restr {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} {α : ↑unitInterval} {s : Set (E × F)} (f : Chart k α s) (t : Set (E × f.Dom)) :

Chart k α s

Restrict a chart to a smaller subset of its domain.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem Moreira2001.Chart.restr_Dom {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} {α : ↑unitInterval} {s : Set (E × F)} (f : Chart k α s) (t : Set (E × f.Dom)) :

(f.restr t).Dom = f.Dom

source

@[simp]

theorem Moreira2001.Chart.restr_instNormedSpaceDom {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} {α : ↑unitInterval} {s : Set (E × F)} (f : Chart k α s) (t : Set (E × f.Dom)) :

(f.restr t).instNormedSpaceDom = f.instNormedSpaceDom

source

@[simp]

theorem Moreira2001.Chart.restr_toFun {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} {α : ↑unitInterval} {s : Set (E × F)} (f : Chart k α s) (t : Set (E × f.Dom)) :

↑(f.restr t) = ↑f

source

@[simp]

theorem Moreira2001.Chart.restr_instNormedAddCommGroupDom {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} {α : ↑unitInterval} {s : Set (E × F)} (f : Chart k α s) (t : Set (E × f.Dom)) :

(f.restr t).instNormedAddCommGroupDom = f.instNormedAddCommGroupDom

source

@[simp]

theorem Moreira2001.Chart.restr_set {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} {α : ↑unitInterval} {s : Set (E × F)} (f : Chart k α s) (t : Set (E × f.Dom)) :

(f.restr t).set = f.set ∩ t

source

def Moreira2001.Chart.ofLE {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} {α : ↑unitInterval} {s : Set (E × F)} (ψ : Chart k α s) (l : ℕ) (hl : l ≤ k) :

Chart l α s

Regard a chart of depth k as a chart of any smaller depth.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem Moreira2001.Chart.ofLE_instNormedSpaceDom {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} {α : ↑unitInterval} {s : Set (E × F)} (ψ : Chart k α s) (l : ℕ) (hl : l ≤ k) :

(ψ.ofLE l hl).instNormedSpaceDom = ψ.instNormedSpaceDom

source

@[simp]

theorem Moreira2001.Chart.ofLE_Dom {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} {α : ↑unitInterval} {s : Set (E × F)} (ψ : Chart k α s) (l : ℕ) (hl : l ≤ k) :

(ψ.ofLE l hl).Dom = ψ.Dom

source

@[simp]

theorem Moreira2001.Chart.ofLE_instNormedAddCommGroupDom {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} {α : ↑unitInterval} {s : Set (E × F)} (ψ : Chart k α s) (l : ℕ) (hl : l ≤ k) :

(ψ.ofLE l hl).instNormedAddCommGroupDom = ψ.instNormedAddCommGroupDom

source

@[simp]

theorem Moreira2001.Chart.ofLE_set {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} {α : ↑unitInterval} {s : Set (E × F)} (ψ : Chart k α s) (l : ℕ) (hl : l ≤ k) :

(ψ.ofLE l hl).set = ψ.set

source

@[simp]

theorem Moreira2001.Chart.ofLE_toFun {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} {α : ↑unitInterval} {s : Set (E × F)} (ψ : Chart k α s) (l : ℕ) (hl : l ≤ k) :

↑(ψ.ofLE l hl) = ↑ψ

source

structure Moreira2001.Atlas {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (k : ℕ) (α : ↑unitInterval) (s : Set (E × F)) :

Type (max u (v + 1))

A countable family of Moreira charts covering the large part of a set.

charts : Set (Chart k α s)
The charts in the atlas.
countable : self.charts.Countable
The atlas is countable.
subset_biUnion_isLargeAt : s ⊆ ⋃ f ∈ self.charts, ↑f '' {x : E × f.Dom | x ∈ f.set ∧ IsLargeAt k α f.set x}
The charts cover s up to the recursively large parts.

Instances For

source

theorem Moreira2001.nonempty_atlas {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {k : ℕ} (hk : k ≠ 0) (α : ↑unitInterval) (s : Set (E × F)) :

Nonempty (Atlas k α s)

source

noncomputable def Moreira2001.Atlas.choice {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] (k : ℕ) (α : ↑unitInterval) (s : Set (E × F)) :

Atlas (k + 1) α s

Choose one atlas supplied by nonempty_atlas.

Equations

Moreira2001.Atlas.choice k α s = Classical.choice ⋯

Instances For

source

def Moreira2001.Atlas.main {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {F : Type v} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] (_k : ℕ) (α : ↑unitInterval) (s : Set (E × F)) :

Atlas 1 α s

The recursive Moreira atlas covering construction.

Equations

One or more equations did not get rendered due to their size.
Moreira2001.Atlas.main 0 x✝¹ x✝ = Moreira2001.Atlas.choice 0 x✝¹ x✝

Instances For