Theorem: image_measure_zero_of_C1_dimension_increase' (Sard/MainTheorem.lean)

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
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

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]
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

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
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

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
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

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
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

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
State after:
no goals