internlm/Lean-Github huggingface dataset:
Theorem: image_null_of_C1_of_dimension_increase
Proof state before:
E : Type u_1
inst✝²⁰ : NormedAddCommGroup E
inst✝¹⁹ : NormedSpace ℝ E
H : Type u_2
inst✝¹⁸ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹⁷ : TopologicalSpace M
inst✝¹⁶ : ChartedSpace H M
inst✝¹⁵ : I.Boundaryless
inst✝¹⁴ : SmoothManifoldWithCorners I M
inst✝¹³ : FiniteDimensional ℝ E
inst✝¹² : SecondCountableTopology M
inst✝¹¹ : MeasurableSpace E
inst✝¹⁰ : BorelSpace E
F : Type u_4
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
G : Type u_5
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
inst✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr : r > m - n
f : M → N
hf : ContMDiff I J (↑r) f
hdim : m < n
x : M
μ : Measure F
hμ : μ.IsAddHaarMeasure
y : N
e : PartialHomeomorph M H := chartAt H x
e' : PartialHomeomorph N G := chartAt G y
⊢ ↑J ∘ ↑e' '' (e'.source ∩ f '' e.source) = ↑J ∘ ↑e' ∘ f '' e.source
Tactic:
sorry
Proof state after:
no goals
Theorem: image_null_of_C1_of_dimension_increase
Proof state before:
E : Type u_1
inst✝²⁰ : NormedAddCommGroup E
inst✝¹⁹ : NormedSpace ℝ E
H : Type u_2
inst✝¹⁸ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹⁷ : TopologicalSpace M
inst✝¹⁶ : ChartedSpace H M
inst✝¹⁵ : I.Boundaryless
inst✝¹⁴ : SmoothManifoldWithCorners I M
inst✝¹³ : FiniteDimensional ℝ E
inst✝¹² : SecondCountableTopology M
inst✝¹¹ : MeasurableSpace E
inst✝¹⁰ : BorelSpace E
F : Type u_4
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
G : Type u_5
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
inst✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr : r > m - n
f : M → N
hf : ContMDiff I J (↑r) f
hdim : m < n
x : M
μ : Measure F
hμ : μ.IsAddHaarMeasure
y : N
e : PartialHomeomorph M H := chartAt H x
e' : PartialHomeomorph N G := chartAt G y
aux : ↑J ∘ ↑e' '' (e'.source ∩ f '' e.source) = ↑J ∘ ↑e' ∘ f '' e.source
g : E → F := ↑J ∘ ↑e' ∘ f ∘ e.invFun ∘ I.invFun
⊢ ↑J ∘ ↑e' ∘ f '' e.source = g '' (↑I '' e.target)
Tactic:
sorry
Proof state after:
no goals
Theorem: image_null_of_C1_of_dimension_increase
Proof state before:
E : Type u_1
inst✝²⁰ : NormedAddCommGroup E
inst✝¹⁹ : NormedSpace ℝ E
H : Type u_2
inst✝¹⁸ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹⁷ : TopologicalSpace M
inst✝¹⁶ : ChartedSpace H M
inst✝¹⁵ : I.Boundaryless
inst✝¹⁴ : SmoothManifoldWithCorners I M
inst✝¹³ : FiniteDimensional ℝ E
inst✝¹² : SecondCountableTopology M
inst✝¹¹ : MeasurableSpace E
inst✝¹⁰ : BorelSpace E
F : Type u_4
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
G : Type u_5
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
inst✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr : r > m - n
f : M → N
hf : ContMDiff I J (↑r) f
hdim : m < n
x : M
μ : Measure F
hμ : μ.IsAddHaarMeasure
y : N
e : PartialHomeomorph M H := chartAt H x
e' : PartialHomeomorph N G := chartAt G y
aux : ↑J ∘ ↑e' '' (e'.source ∩ f '' e.source) = ↑J ∘ ↑e' ∘ f '' e.source
g : E → F := ↑J ∘ ↑e' ∘ f ∘ e.invFun ∘ I.invFun
this : ↑J ∘ ↑e' ∘ f '' e.source = g '' (↑I '' e.target)
⊢ IsOpen (↑I '' e.target)
Tactic:
sorry
Proof state after:
no goals
Theorem: image_null_of_C1_of_dimension_increase
Proof state before:
E : Type u_1
inst✝²⁰ : NormedAddCommGroup E
inst✝¹⁹ : NormedSpace ℝ E
H : Type u_2
inst✝¹⁸ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹⁷ : TopologicalSpace M
inst✝¹⁶ : ChartedSpace H M
inst✝¹⁵ : I.Boundaryless
inst✝¹⁴ : SmoothManifoldWithCorners I M
inst✝¹³ : FiniteDimensional ℝ E
inst✝¹² : SecondCountableTopology M
inst✝¹¹ : MeasurableSpace E
inst✝¹⁰ : BorelSpace E
F : Type u_4
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
G : Type u_5
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
inst✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr : r > m - n
f : M → N
hf : ContMDiff I J (↑r) f
hdim : m < n
x : M
μ : Measure F
hμ : μ.IsAddHaarMeasure
y : N
e : PartialHomeomorph M H := chartAt H x
e' : PartialHomeomorph N G := chartAt G y
aux : ↑J ∘ ↑e' '' (e'.source ∩ f '' e.source) = ↑J ∘ ↑e' ∘ f '' e.source
g : E → F := ↑J ∘ ↑e' ∘ f ∘ e.invFun ∘ I.invFun
this : ↑J ∘ ↑e' ∘ f '' e.source = g '' (↑I '' e.target)
hopen : IsOpen (↑I '' e.target)
⊢ ContDiffOn ℝ 1 g (↑I '' e.target)
Tactic:
sorry
Proof state after:
no goals
Theorem: image_measure_zero_of_C1_dimension_increase'
Proof state before:
E : Type u_1
inst✝²¹ : NormedAddCommGroup E
inst✝²⁰ : NormedSpace ℝ E
H : Type u_2
inst✝¹⁹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹⁸ : TopologicalSpace M
inst✝¹⁷ : ChartedSpace H M
inst✝¹⁶ : SmoothManifoldWithCorners I M
inst✝¹⁵ : FiniteDimensional ℝ E
inst✝¹⁴ : SecondCountableTopology M
inst✝¹³ : MeasurableSpace E
inst✝¹² : BorelSpace E
F : Type u_4
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace ℝ F
G : Type u_5
inst✝⁹ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁸ : TopologicalSpace N
inst✝⁷ : ChartedSpace G N
inst✝⁶ : SmoothManifoldWithCorners J N
inst✝⁵ : FiniteDimensional ℝ F
inst✝⁴ : MeasurableSpace F
inst✝³ : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr : r > m - n
g : E → F
U : Set E
hU : IsOpen U
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
ν : Measure F
inst✝ : ν.IsAddHaarMeasure
hg : ContDiffOn ℝ 1 g U
hmn : m < n
⊢ ↑ν (g '' U) = 0
Tactic:
have h : ν = μH[n] := sorry
Proof state after:
E : Type u_1
inst✝²¹ : NormedAddCommGroup E
inst✝²⁰ : NormedSpace ℝ E
H : Type u_2
inst✝¹⁹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹⁸ : TopologicalSpace M
inst✝¹⁷ : ChartedSpace H M
inst✝¹⁶ : SmoothManifoldWithCorners I M
inst✝¹⁵ : FiniteDimensional ℝ E
inst✝¹⁴ : SecondCountableTopology M
inst✝¹³ : MeasurableSpace E
inst✝¹² : BorelSpace E
F : Type u_4
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace ℝ F
G : Type u_5
inst✝⁹ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁸ : TopologicalSpace N
inst✝⁷ : ChartedSpace G N
inst✝⁶ : SmoothManifoldWithCorners J N
inst✝⁵ : FiniteDimensional ℝ F
inst✝⁴ : MeasurableSpace F
inst✝³ : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr : r > m - n
g : E → F
U : Set E
hU : IsOpen U
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
ν : Measure F
inst✝ : ν.IsAddHaarMeasure
hg : ContDiffOn ℝ 1 g U
hmn : m < n
h : ν = μH[↑n]
⊢ ↑ν (g '' U) = 0
Theorem: image_measure_zero_of_C1_dimension_increase'
Proof state before:
E : Type u_1
inst✝²¹ : NormedAddCommGroup E
inst✝²⁰ : NormedSpace ℝ E
H : Type u_2
inst✝¹⁹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹⁸ : TopologicalSpace M
inst✝¹⁷ : ChartedSpace H M
inst✝¹⁶ : SmoothManifoldWithCorners I M
inst✝¹⁵ : FiniteDimensional ℝ E
inst✝¹⁴ : SecondCountableTopology M
inst✝¹³ : MeasurableSpace E
inst✝¹² : BorelSpace E
F : Type u_4
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace ℝ F
G : Type u_5
inst✝⁹ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁸ : TopologicalSpace N
inst✝⁷ : ChartedSpace G N
inst✝⁶ : SmoothManifoldWithCorners J N
inst✝⁵ : FiniteDimensional ℝ F
inst✝⁴ : MeasurableSpace F
inst✝³ : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr : r > m - n
g : E → F
U : Set E
hU : IsOpen U
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
ν : Measure F
inst✝ : ν.IsAddHaarMeasure
hg : ContDiffOn ℝ 1 g U
hmn : m < n
h : ν = μH[↑n]
⊢ ↑ν (g '' U) = 0
Tactic:
rw [h]
Proof state after:
E : Type u_1
inst✝²¹ : NormedAddCommGroup E
inst✝²⁰ : NormedSpace ℝ E
H : Type u_2
inst✝¹⁹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹⁸ : TopologicalSpace M
inst✝¹⁷ : ChartedSpace H M
inst✝¹⁶ : SmoothManifoldWithCorners I M
inst✝¹⁵ : FiniteDimensional ℝ E
inst✝¹⁴ : SecondCountableTopology M
inst✝¹³ : MeasurableSpace E
inst✝¹² : BorelSpace E
F : Type u_4
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace ℝ F
G : Type u_5
inst✝⁹ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁸ : TopologicalSpace N
inst✝⁷ : ChartedSpace G N
inst✝⁶ : SmoothManifoldWithCorners J N
inst✝⁵ : FiniteDimensional ℝ F
inst✝⁴ : MeasurableSpace F
inst✝³ : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr : r > m - n
g : E → F
U : Set E
hU : IsOpen U
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
ν : Measure F
inst✝ : ν.IsAddHaarMeasure
hg : ContDiffOn ℝ 1 g U
hmn : m < n
h : ν = μH[↑n]
⊢ ↑μH[↑n] (g '' U) = 0
Theorem: image_measure_zero_of_C1_dimension_increase'
Proof state before:
E : Type u_1
inst✝²¹ : NormedAddCommGroup E
inst✝²⁰ : NormedSpace ℝ E
H : Type u_2
inst✝¹⁹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹⁸ : TopologicalSpace M
inst✝¹⁷ : ChartedSpace H M
inst✝¹⁶ : SmoothManifoldWithCorners I M
inst✝¹⁵ : FiniteDimensional ℝ E
inst✝¹⁴ : SecondCountableTopology M
inst✝¹³ : MeasurableSpace E
inst✝¹² : BorelSpace E
F : Type u_4
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace ℝ F
G : Type u_5
inst✝⁹ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁸ : TopologicalSpace N
inst✝⁷ : ChartedSpace G N
inst✝⁶ : SmoothManifoldWithCorners J N
inst✝⁵ : FiniteDimensional ℝ F
inst✝⁴ : MeasurableSpace F
inst✝³ : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr : r > m - n
g : E → F
U : Set E
hU : IsOpen U
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
ν : Measure F
inst✝ : ν.IsAddHaarMeasure
hg : ContDiffOn ℝ 1 g U
hmn : m < n
h : ν = μH[↑n]
⊢ ↑μH[↑n] (g '' U) = 0
Tactic:
have : Convex ℝ U := sorry
Proof state after:
E : Type u_1
inst✝²¹ : NormedAddCommGroup E
inst✝²⁰ : NormedSpace ℝ E
H : Type u_2
inst✝¹⁹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹⁸ : TopologicalSpace M
inst✝¹⁷ : ChartedSpace H M
inst✝¹⁶ : SmoothManifoldWithCorners I M
inst✝¹⁵ : FiniteDimensional ℝ E
inst✝¹⁴ : SecondCountableTopology M
inst✝¹³ : MeasurableSpace E
inst✝¹² : BorelSpace E
F : Type u_4
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace ℝ F
G : Type u_5
inst✝⁹ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁸ : TopologicalSpace N
inst✝⁷ : ChartedSpace G N
inst✝⁶ : SmoothManifoldWithCorners J N
inst✝⁵ : FiniteDimensional ℝ F
inst✝⁴ : MeasurableSpace F
inst✝³ : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr : r > m - n
g : E → F
U : Set E
hU : IsOpen U
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
ν : Measure F
inst✝ : ν.IsAddHaarMeasure
hg : ContDiffOn ℝ 1 g U
hmn : m < n
h : ν = μH[↑n]
this : Convex ℝ U
⊢ ↑μH[↑n] (g '' U) = 0
Theorem: image_measure_zero_of_C1_dimension_increase'
Proof state before:
E : Type u_1
inst✝²¹ : NormedAddCommGroup E
inst✝²⁰ : NormedSpace ℝ E
H : Type u_2
inst✝¹⁹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹⁸ : TopologicalSpace M
inst✝¹⁷ : ChartedSpace H M
inst✝¹⁶ : SmoothManifoldWithCorners I M
inst✝¹⁵ : FiniteDimensional ℝ E
inst✝¹⁴ : SecondCountableTopology M
inst✝¹³ : MeasurableSpace E
inst✝¹² : BorelSpace E
F : Type u_4
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace ℝ F
G : Type u_5
inst✝⁹ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁸ : TopologicalSpace N
inst✝⁷ : ChartedSpace G N
inst✝⁶ : SmoothManifoldWithCorners J N
inst✝⁵ : FiniteDimensional ℝ F
inst✝⁴ : MeasurableSpace F
inst✝³ : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr : r > m - n
g : E → F
U : Set E
hU : IsOpen U
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
ν : Measure F
inst✝ : ν.IsAddHaarMeasure
hg : ContDiffOn ℝ 1 g U
hmn : m < n
h : ν = μH[↑n]
this : Convex ℝ U
⊢ ↑μH[↑n] (g '' U) = 0
Tactic:
have h : dimH (univ : Set E) = m := sorry
Proof state after:
E : Type u_1
inst✝²¹ : NormedAddCommGroup E
inst✝²⁰ : NormedSpace ℝ E
H : Type u_2
inst✝¹⁹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹⁸ : TopologicalSpace M
inst✝¹⁷ : ChartedSpace H M
inst✝¹⁶ : SmoothManifoldWithCorners I M
inst✝¹⁵ : FiniteDimensional ℝ E
inst✝¹⁴ : SecondCountableTopology M
inst✝¹³ : MeasurableSpace E
inst✝¹² : BorelSpace E
F : Type u_4
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace ℝ F
G : Type u_5
inst✝⁹ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁸ : TopologicalSpace N
inst✝⁷ : ChartedSpace G N
inst✝⁶ : SmoothManifoldWithCorners J N
inst✝⁵ : FiniteDimensional ℝ F
inst✝⁴ : MeasurableSpace F
inst✝³ : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr : r > m - n
g : E → F
U : Set E
hU : IsOpen U
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
ν : Measure F
inst✝ : ν.IsAddHaarMeasure
hg : ContDiffOn ℝ 1 g U
hmn : m < n
h✝ : ν = μH[↑n]
this : Convex ℝ U
h : dimH univ = ↑m
⊢ ↑μH[↑n] (g '' U) = 0
Theorem: image_measure_zero_of_C1_dimension_increase'
Proof state before:
E : Type u_1
inst✝²¹ : NormedAddCommGroup E
inst✝²⁰ : NormedSpace ℝ E
H : Type u_2
inst✝¹⁹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹⁸ : TopologicalSpace M
inst✝¹⁷ : ChartedSpace H M
inst✝¹⁶ : SmoothManifoldWithCorners I M
inst✝¹⁵ : FiniteDimensional ℝ E
inst✝¹⁴ : SecondCountableTopology M
inst✝¹³ : MeasurableSpace E
inst✝¹² : BorelSpace E
F : Type u_4
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace ℝ F
G : Type u_5
inst✝⁹ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁸ : TopologicalSpace N
inst✝⁷ : ChartedSpace G N
inst✝⁶ : SmoothManifoldWithCorners J N
inst✝⁵ : FiniteDimensional ℝ F
inst✝⁴ : MeasurableSpace F
inst✝³ : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr : r > m - n
g : E → F
U : Set E
hU : IsOpen U
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
ν : Measure F
inst✝ : ν.IsAddHaarMeasure
hg : ContDiffOn ℝ 1 g U
hmn : m < n
h✝ : ν = μH[↑n]
this : Convex ℝ U
h : dimH univ = ↑m
⊢ ↑μH[↑n] (g '' U) = 0
Tactic:
apply measure_zero_of_dimH_lt (d := n) rfl.absolutelyContinuous
Proof state after:
E : Type u_1
inst✝²¹ : NormedAddCommGroup E
inst✝²⁰ : NormedSpace ℝ E
H : Type u_2
inst✝¹⁹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹⁸ : TopologicalSpace M
inst✝¹⁷ : ChartedSpace H M
inst✝¹⁶ : SmoothManifoldWithCorners I M
inst✝¹⁵ : FiniteDimensional ℝ E
inst✝¹⁴ : SecondCountableTopology M
inst✝¹³ : MeasurableSpace E
inst✝¹² : BorelSpace E
F : Type u_4
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace ℝ F
G : Type u_5
inst✝⁹ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁸ : TopologicalSpace N
inst✝⁷ : ChartedSpace G N
inst✝⁶ : SmoothManifoldWithCorners J N
inst✝⁵ : FiniteDimensional ℝ F
inst✝⁴ : MeasurableSpace F
inst✝³ : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr : r > m - n
g : E → F
U : Set E
hU : IsOpen U
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
ν : Measure F
inst✝ : ν.IsAddHaarMeasure
hg : ContDiffOn ℝ 1 g U
hmn : m < n
h✝ : ν = μH[↑n]
this : Convex ℝ U
h : dimH univ = ↑m
⊢ dimH (g '' U) < ↑↑n
Theorem: image_measure_zero_of_C1_dimension_increase'
Proof state before:
E : Type u_1
inst✝²¹ : NormedAddCommGroup E
inst✝²⁰ : NormedSpace ℝ E
H : Type u_2
inst✝¹⁹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹⁸ : TopologicalSpace M
inst✝¹⁷ : ChartedSpace H M
inst✝¹⁶ : SmoothManifoldWithCorners I M
inst✝¹⁵ : FiniteDimensional ℝ E
inst✝¹⁴ : SecondCountableTopology M
inst✝¹³ : MeasurableSpace E
inst✝¹² : BorelSpace E
F : Type u_4
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace ℝ F
G : Type u_5
inst✝⁹ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁸ : TopologicalSpace N
inst✝⁷ : ChartedSpace G N
inst✝⁶ : SmoothManifoldWithCorners J N
inst✝⁵ : FiniteDimensional ℝ F
inst✝⁴ : MeasurableSpace F
inst✝³ : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr : r > m - n
g : E → F
U : Set E
hU : IsOpen U
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
ν : Measure F
inst✝ : ν.IsAddHaarMeasure
hg : ContDiffOn ℝ 1 g U
hmn : m < n
h✝ : ν = μH[↑n]
this : Convex ℝ U
h : dimH univ = ↑m
⊢ dimH (g '' U) < ↑↑n
Tactic:
calc dimH (g '' U)
  _ ≤ dimH U := hg.dimH_image_le this rfl.subset
  _ ≤ m := h ▸ dimH_mono (subset_univ U) _ < n := Nat.cast_lt.mpr hmn
Proof state after:
no goals
Theorem: sard_local
Proof state before:
E : Type u_1
inst✝¹⁹ : NormedAddCommGroup E
inst✝¹⁸ : NormedSpace ℝ E
H : Type u_2
inst✝¹⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹⁶ : TopologicalSpace M
inst✝¹⁵ : ChartedSpace H M
inst✝¹⁴ : SmoothManifoldWithCorners I M
inst✝¹³ : FiniteDimensional ℝ E
inst✝¹² : SecondCountableTopology M
inst✝¹¹ : MeasurableSpace E
inst✝¹⁰ : BorelSpace E
F : Type u_4
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
G : Type u_5
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
inst✝⁴ : SmoothManifoldWithCorners J N
inst✝³ : FiniteDimensional ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr : r > m - n
s w : Set E
f : E → F
hw : IsOpen w
hsw : s ⊆ w
hf : ContDiffOn ℝ (↑r) f w
f' : E → E →L[ℝ] F
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) w x
h'f' : ∀ x ∈ s, ¬Surjective ⇑(f' x)
μ : Measure F
inst✝ : μ.IsAddHaarMeasure
⊢ ↑μ (f '' s) = 0
Tactic:
by_cases hyp: m < n
Proof state after:
case pos
E : Type u_1
inst✝¹⁹ : NormedAddCommGroup E
inst✝¹⁸ : NormedSpace ℝ E
H : Type u_2
inst✝¹⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹⁶ : TopologicalSpace M
inst✝¹⁵ : ChartedSpace H M
inst✝¹⁴ : SmoothManifoldWithCorners I M
inst✝¹³ : FiniteDimensional ℝ E
inst✝¹² : SecondCountableTopology M
inst✝¹¹ : MeasurableSpace E
inst✝¹⁰ : BorelSpace E
F : Type u_4
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
G : Type u_5
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
inst✝⁴ : SmoothManifoldWithCorners J N
inst✝³ : FiniteDimensional ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr : r > m - n
s w : Set E
f : E → F
hw : IsOpen w
hsw : s ⊆ w
hf : ContDiffOn ℝ (↑r) f w
f' : E → E →L[ℝ] F
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) w x
h'f' : ∀ x ∈ s, ¬Surjective ⇑(f' x)
μ : Measure F
inst✝ : μ.IsAddHaarMeasure
hyp : m < n
⊢ ↑μ (f '' s) = 0

case neg
E : Type u_1
inst✝¹⁹ : NormedAddCommGroup E
inst✝¹⁸ : NormedSpace ℝ E
H : Type u_2
inst✝¹⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹⁶ : TopologicalSpace M
inst✝¹⁵ : ChartedSpace H M
inst✝¹⁴ : SmoothManifoldWithCorners I M
inst✝¹³ : FiniteDimensional ℝ E
inst✝¹² : SecondCountableTopology M
inst✝¹¹ : MeasurableSpace E
inst✝¹⁰ : BorelSpace E
F : Type u_4
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
G : Type u_5
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
inst✝⁴ : SmoothManifoldWithCorners J N
inst✝³ : FiniteDimensional ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr : r > m - n
s w : Set E
f : E → F
hw : IsOpen w
hsw : s ⊆ w
hf : ContDiffOn ℝ (↑r) f w
f' : E → E →L[ℝ] F
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) w x
h'f' : ∀ x ∈ s, ¬Surjective ⇑(f' x)
μ : Measure F
inst✝ : μ.IsAddHaarMeasure
hyp : ¬m < n
⊢ ↑μ (f '' s) = 0
Theorem: sard_local
Proof state before:
case pos
E : Type u_1
inst✝¹⁹ : NormedAddCommGroup E
inst✝¹⁸ : NormedSpace ℝ E
H : Type u_2
inst✝¹⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹⁶ : TopologicalSpace M
inst✝¹⁵ : ChartedSpace H M
inst✝¹⁴ : SmoothManifoldWithCorners I M
inst✝¹³ : FiniteDimensional ℝ E
inst✝¹² : SecondCountableTopology M
inst✝¹¹ : MeasurableSpace E
inst✝¹⁰ : BorelSpace E
F : Type u_4
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
G : Type u_5
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
inst✝⁴ : SmoothManifoldWithCorners J N
inst✝³ : FiniteDimensional ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr : r > m - n
s w : Set E
f : E → F
hw : IsOpen w
hsw : s ⊆ w
hf : ContDiffOn ℝ (↑r) f w
f' : E → E →L[ℝ] F
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) w x
h'f' : ∀ x ∈ s, ¬Surjective ⇑(f' x)
μ : Measure F
inst✝ : μ.IsAddHaarMeasure
hyp : m < n
⊢ ↑μ (f '' s) = 0
Tactic:
have hr : 1 ≤ (r : ℕ∞) := Nat.one_le_cast.mpr (Nat.one_le_of_lt hr)
Proof state after:
case pos
E : Type u_1
inst✝¹⁹ : NormedAddCommGroup E
inst✝¹⁸ : NormedSpace ℝ E
H : Type u_2
inst✝¹⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹⁶ : TopologicalSpace M
inst✝¹⁵ : ChartedSpace H M
inst✝¹⁴ : SmoothManifoldWithCorners I M
inst✝¹³ : FiniteDimensional ℝ E
inst✝¹² : SecondCountableTopology M
inst✝¹¹ : MeasurableSpace E
inst✝¹⁰ : BorelSpace E
F : Type u_4
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
G : Type u_5
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
inst✝⁴ : SmoothManifoldWithCorners J N
inst✝³ : FiniteDimensional ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr✝ : r > m - n
s w : Set E
f : E → F
hw : IsOpen w
hsw : s ⊆ w
hf : ContDiffOn ℝ (↑r) f w
f' : E → E →L[ℝ] F
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) w x
h'f' : ∀ x ∈ s, ¬Surjective ⇑(f' x)
μ : Measure F
inst✝ : μ.IsAddHaarMeasure
hyp : m < n
hr : 1 ≤ ↑r
⊢ ↑μ (f '' s) = 0
Theorem: sard_local
Proof state before:
case pos
E : Type u_1
inst✝¹⁹ : NormedAddCommGroup E
inst✝¹⁸ : NormedSpace ℝ E
H : Type u_2
inst✝¹⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹⁶ : TopologicalSpace M
inst✝¹⁵ : ChartedSpace H M
inst✝¹⁴ : SmoothManifoldWithCorners I M
inst✝¹³ : FiniteDimensional ℝ E
inst✝¹² : SecondCountableTopology M
inst✝¹¹ : MeasurableSpace E
inst✝¹⁰ : BorelSpace E
F : Type u_4
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
G : Type u_5
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
inst✝⁴ : SmoothManifoldWithCorners J N
inst✝³ : FiniteDimensional ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr✝ : r > m - n
s w : Set E
f : E → F
hw : IsOpen w
hsw : s ⊆ w
hf : ContDiffOn ℝ (↑r) f w
f' : E → E →L[ℝ] F
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) w x
h'f' : ∀ x ∈ s, ¬Surjective ⇑(f' x)
μ : Measure F
inst✝ : μ.IsAddHaarMeasure
hyp : m < n
hr : 1 ≤ ↑r
⊢ ↑μ (f '' s) = 0
Tactic:
have hless: μ (f '' s) ≤ 0 := calc
  μ (f '' s)
  _ ≤ μ (f '' w) := measure_mono (image_subset f hsw)
  _ = 0 := image_measure_zero_of_C1_dimension_increase' hw μ (hf.of_le hr) hyp
Proof state after:
case pos
E : Type u_1
inst✝¹⁹ : NormedAddCommGroup E
inst✝¹⁸ : NormedSpace ℝ E
H : Type u_2
inst✝¹⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹⁶ : TopologicalSpace M
inst✝¹⁵ : ChartedSpace H M
inst✝¹⁴ : SmoothManifoldWithCorners I M
inst✝¹³ : FiniteDimensional ℝ E
inst✝¹² : SecondCountableTopology M
inst✝¹¹ : MeasurableSpace E
inst✝¹⁰ : BorelSpace E
F : Type u_4
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
G : Type u_5
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
inst✝⁴ : SmoothManifoldWithCorners J N
inst✝³ : FiniteDimensional ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr✝ : r > m - n
s w : Set E
f : E → F
hw : IsOpen w
hsw : s ⊆ w
hf : ContDiffOn ℝ (↑r) f w
f' : E → E →L[ℝ] F
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) w x
h'f' : ∀ x ∈ s, ¬Surjective ⇑(f' x)
μ : Measure F
inst✝ : μ.IsAddHaarMeasure
hyp : m < n
hr : 1 ≤ ↑r
hless : ↑μ (f '' s) ≤ 0
⊢ ↑μ (f '' s) = 0