Theorem: Measure_theory.Lp_trim_to_Lp.isometry (Untitled/Probability/Indep.lean)

State before:
α : Type u_1
m1 m2 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
hm : m1 ≤ m2
T : Fact (1 ≤ p)
⊢ Isometry (Lp_trim_to_Lp p μ hm)
Tactic:
rintro f g
State after:
α : Type u_1
m1 m2 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
hm : m1 ≤ m2
T : Fact (1 ≤ p)
f g : ↥(Lp ℝ p)
⊢ edist (Lp_trim_to_Lp p μ hm f) (Lp_trim_to_Lp p μ hm g) = edist f g

State before:
α : Type u_1
m1 m2 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
hm : m1 ≤ m2
T : Fact (1 ≤ p)
f g : ↥(Lp ℝ p)
⊢ edist (Lp_trim_to_Lp p μ hm f) (Lp_trim_to_Lp p μ hm g) = edist f g
Tactic:
rw [Lp.edist_def, Lp.edist_def]
State after:
α : Type u_1
m1 m2 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
hm : m1 ≤ m2
T : Fact (1 ≤ p)
f g : ↥(Lp ℝ p)
⊢ MeasureTheory.snorm (↑↑(Lp_trim_to_Lp p μ hm f) - ↑↑(Lp_trim_to_Lp p μ hm g)) p μ =
    MeasureTheory.snorm (↑↑f - ↑↑g) p (Measure.trim μ hm)

State before:
α : Type u_1
m1 m2 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
hm : m1 ≤ m2
T : Fact (1 ≤ p)
f g : ↥(Lp ℝ p)
⊢ MeasureTheory.snorm (↑↑(Lp_trim_to_Lp p μ hm f) - ↑↑(Lp_trim_to_Lp p μ hm g)) p μ =
    MeasureTheory.snorm (↑↑f - ↑↑g) p (Measure.trim μ hm)
Tactic:
rw [snorm_trim_ae hm ((Lp.aestronglyMeasurable f).sub (Lp.aestronglyMeasurable g))]
State after:
α : Type u_1
m1 m2 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
hm : m1 ≤ m2
T : Fact (1 ≤ p)
f g : ↥(Lp ℝ p)
⊢ MeasureTheory.snorm (↑↑(Lp_trim_to_Lp p μ hm f) - ↑↑(Lp_trim_to_Lp p μ hm g)) p μ =
    MeasureTheory.snorm (↑↑f - ↑↑g) p μ

State before:
α : Type u_1
m1 m2 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
hm : m1 ≤ m2
T : Fact (1 ≤ p)
f g : ↥(Lp ℝ p)
⊢ MeasureTheory.snorm (↑↑(Lp_trim_to_Lp p μ hm f) - ↑↑(Lp_trim_to_Lp p μ hm g)) p μ =
    MeasureTheory.snorm (↑↑f - ↑↑g) p μ
Tactic:
exact snorm_congr_ae (ae_eq.sub ae_eq)
State after:
no goals