awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
h_meas_Ioo :
  ¬∃ (a : ℝ),
      0 < a ∧
        LT.lt (α := ℝ≥0∞) (2⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) ∧
          LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)
⊢ ∃ (C : ℝ), 0 < C ∧ Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) μ
have neg : ∀ (b : ℝ) (hb : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ b} : ℝ≥0∞) (1 : ℝ≥0∞)),
  ∃ (C : ℝ), 0 < C ∧ Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) μ
Tactic: obtain ⟨b, hb⟩ : ∃ b, μ {x | ‖x‖ ≤ b} = 1 := by
    by_contra h_ne
    push Not at h_meas_Ioo h_ne
    suffices μ .univ ≤ 2⁻¹ by simp at this
    have h_le a : μ {x | ‖x‖ ≤ a} ≤ 2⁻¹ := by
      have h_of_pos a' (ha : 0 < a') : μ {x | ‖x‖ ≤ a'} ≤ 2⁻¹ := by
        by_contra h_lt
        refine h_ne a' ?_
        exact le_antisymm prob_le_one (h_meas_Ioo a' ha (not_le.mp h_lt))
      rcases le_or_gt a 0 with ha | ha
      · calc μ {x | ‖x‖ ≤ a}
        _ ≤ μ {x | ‖x‖ ≤ 1} := measure_mono fun x hx ↦ hx.trans (ha.trans (by positivity))
        _ ≤ 2⁻¹ := h_of_pos _ (by positivity)
      · exact h_of_pos a ha
    have h_univ : (Set.univ : Set E) = ⋃ a : ℕ, {x | ‖x‖ ≤ a} := by
      ext x
      simp only [Set.mem_univ, Set.mem_iUnion, Set.mem_setOf_eq, true_iff]
      exact exists_nat_ge _
    rw [h_univ, Monotone.measure_iUnion]
    · simp [h_le]
    · intro a b hab x hx
      simp only [Set.mem_setOf_eq] at hx ⊢
      exact hx.trans (mod_cast hab)
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
h_meas_Ioo :
  ¬∃ (a : ℝ),
      0 < a ∧
        LT.lt (α := ℝ≥0∞) (2⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) ∧
          LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)
b : ℝ
hb : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ b} : ℝ≥0∞) (1 : ℝ≥0∞)
⊢ ∀ᵐ (x : E) ∂μ, ‖x‖ ≤ b
have rwa : Measurable (β := Prop) fun (x : E) ↦ ‖x‖ ≤ b
Tactic: rwa [ae_iff_prob_eq_one]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
h_meas_Ioo :
  ¬∃ (a : ℝ),
      0 < a ∧
        LT.lt (α := ℝ≥0∞) (2⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) ∧
          LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)
b : ℝ
hb : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ b} : ℝ≥0∞) (1 : ℝ≥0∞)
⊢ Measurable (β := Prop) fun (x : E) ↦ ‖x‖ ≤ b
have refine : MeasurableSet.{u_1} (α := E) (Set.preimage (β := Prop) (fun (x : E) ↦ ‖x‖ ≤ b) {True})
Tactic: refine measurable_to_prop ?_
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
h_meas_Ioo :
  ¬∃ (a : ℝ),
      0 < a ∧
        LT.lt (α := ℝ≥0∞) (2⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) ∧
          LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)
b : ℝ
hb : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ b} : ℝ≥0∞) (1 : ℝ≥0∞)
⊢ Eq.{u_1 + 1} (α := Set E) (Set.preimage (β := Prop) (fun (x : E) ↦ ‖x‖ ≤ b) {True}) {x : E | ‖x‖ ≤ b}
have h : ∀ (x : E),
  Membership.mem (γ := Set E) (Set.preimage (β := Prop) (fun (x : E) ↦ ‖x‖ ≤ b) {True}) x ↔
    Membership.mem (γ := Set E) {x : E | ‖x‖ ≤ b} x
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
h_meas_Ioo :
  ¬∃ (a : ℝ),
      0 < a ∧
        LT.lt (α := ℝ≥0∞) (2⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) ∧
          LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)
b : ℝ
hb : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ b} : ℝ≥0∞) (1 : ℝ≥0∞)
⊢ MeasurableSet.{u_1} (α := E) (Set.preimage (β := Prop) (fun (x : E) ↦ ‖x‖ ≤ b) {True})
have rw : MeasurableSet.{u_1} (α := E) {x : E | ‖x‖ ≤ b}
Tactic: rw [show (fun x : E ↦ ‖x‖ ≤ b) ⁻¹' {True} = {x : E | ‖x‖ ≤ b} by ext; simp]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
h_meas_Ioo :
  ¬∃ (a : ℝ),
      0 < a ∧
        LT.lt (α := ℝ≥0∞) (2⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) ∧
          LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)
b : ℝ
hb : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ b} : ℝ≥0∞) (1 : ℝ≥0∞)
⊢ Measurable.{u_1, 0} (α := E) norm
have funProp : inst_3 ≤ inst_3
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
h_meas_Ioo :
  ¬∃ (a : ℝ),
      0 < a ∧
        LT.lt (α := ℝ≥0∞) (2⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) ∧
          LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)
b : ℝ
hb : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ b} : ℝ≥0∞) (1 : ℝ≥0∞)
funProp : inst_3 ≤ inst_3
⊢ Measurable.{u_1, 0} (α := E) norm
have funProp₁ : MeasurableEmbedding (β := ℝ) fun (a : E) ↦ ‖a‖
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (hypothesis)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
h_meas_Ioo :
  ¬∃ (a : ℝ),
      0 < a ∧
        LT.lt (α := ℝ≥0∞) (2⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) ∧
          LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)
b : ℝ
hb : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ b} : ℝ≥0∞) (1 : ℝ≥0∞)
⊢ ∃ (C : ℝ), 0 < C ∧ Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) μ
have hb' : ∀ᵐ (x : E) ∂μ, ‖x‖ ≤ b
Tactic: have hb' : ∀ᵐ x ∂μ, ‖x‖ ≤ b := by
    rwa [ae_iff_prob_eq_one]
    refine measurable_to_prop ?_
    rw [show (fun x : E ↦ ‖x‖ ≤ b) ⁻¹' {True} = {x : E | ‖x‖ ≤ b} by ext; simp]
    exact measurableSet_le (by fun_prop) (by fun_prop)
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
h_meas_Ioo :
  ¬∃ (a : ℝ),
      0 < a ∧
        LT.lt (α := ℝ≥0∞) (2⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) ∧
          LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)
b : ℝ
hb : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ b} : ℝ≥0∞) (1 : ℝ≥0∞)
hb' : ∀ᵐ (x : E) ∂μ, ‖x‖ ≤ b
⊢ ∃ (C : ℝ), 0 < C ∧ Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) μ
have neg : Integrable (ε := ℝ) (fun (x : E) ↦ rexp (1 * HPow.hPow (β := ℕ) ‖x‖ 2)) μ
Tactic: refine ⟨1, by positivity, ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
h_meas_Ioo :
  ¬∃ (a : ℝ),
      0 < a ∧
        LT.lt (α := ℝ≥0∞) (2⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) ∧
          LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)
b : ℝ
hb : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ b} : ℝ≥0∞) (1 : ℝ≥0∞)
hb' : ∀ᵐ (x : E) ∂μ, ‖x‖ ≤ b
⊢ Integrable (ε := ℝ) (fun (x : E) ↦ rexp (1 * HPow.hPow (β := ℕ) ‖x‖ 2)) μ
have neg : (ae μ).EventuallyLE (β := ℝ) 0 fun (x : E) ↦ rexp (1 * HPow.hPow (β := ℕ) ‖x‖ 2)
Tactic: refine integrable_of_le_of_le (g₁ := 0) (g₂ := fun _ ↦ rexp (b ^ 2)) (by fun_prop)
    ?_ ?_ (integrable_const _) (integrable_const _)
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
h_meas_Ioo :
  ¬∃ (a : ℝ),
      0 < a ∧
        LT.lt (α := ℝ≥0∞) (2⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) ∧
          LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)
b : ℝ
hb : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ b} : ℝ≥0∞) (1 : ℝ≥0∞)
hb' : ∀ᵐ (x : E) ∂μ, ‖x‖ ≤ b
neg : (ae μ).EventuallyLE (β := ℝ) 0 fun (x : E) ↦ rexp (1 * HPow.hPow (β := ℕ) ‖x‖ 2)
⊢ Integrable (ε := ℝ) (fun (x : E) ↦ rexp (1 * HPow.hPow (β := ℕ) ‖x‖ 2)) μ
have neg₁ : (ae μ).EventuallyLE (β := ℝ) (fun (x : E) ↦ rexp (1 * HPow.hPow (β := ℕ) ‖x‖ 2)) fun (x : E) ↦
  rexp (HPow.hPow (β := ℕ) b 2)
Tactic: refine integrable_of_le_of_le (g₁ := 0) (g₂ := fun _ ↦ rexp (b ^ 2)) (by fun_prop)
    ?_ ?_ (integrable_const _) (integrable_const _)
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
h_meas_Ioo :
  ¬∃ (a : ℝ),
      0 < a ∧
        LT.lt (α := ℝ≥0∞) (2⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) ∧
          LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)
b : ℝ
hb : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ b} : ℝ≥0∞) (1 : ℝ≥0∞)
hb' : ∀ᵐ (x : E) ∂μ, ‖x‖ ≤ b
⊢ (ae μ).EventuallyLE (β := ℝ) (fun (x : E) ↦ rexp (1 * HPow.hPow (β := ℕ) ‖x‖ 2)) fun (x : E) ↦
    rexp (HPow.hPow (β := ℕ) b 2)
have h : ∀ (x : E) (hx : ‖x‖ ≤ b), rexp (1 * HPow.hPow (β := ℕ) ‖x‖ 2) ≤ rexp (HPow.hPow (β := ℕ) b 2)
Tactic: filter_upwards [hb'] with x hx
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
h_meas_Ioo :
  ¬∃ (a : ℝ),
      0 < a ∧
        LT.lt (α := ℝ≥0∞) (2⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) ∧
          LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)
b : ℝ
hb : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ b} : ℝ≥0∞) (1 : ℝ≥0∞)
hb' : ∀ᵐ (x : E) ∂μ, ‖x‖ ≤ b
x : E
hx : ‖x‖ ≤ b
⊢ rexp (1 * HPow.hPow (β := ℕ) ‖x‖ 2) ≤ rexp (HPow.hPow (β := ℕ) b 2)
have h : rexp (HPow.hPow (β := ℕ) ‖x‖ 2) ≤ rexp (HPow.hPow (β := ℕ) b 2)
Tactic: simp only [one_mul]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
h_meas_Ioo :
  ¬∃ (a : ℝ),
      0 < a ∧
        LT.lt (α := ℝ≥0∞) (2⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) ∧
          LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)
b : ℝ
hb : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ b} : ℝ≥0∞) (1 : ℝ≥0∞)
hb' : ∀ᵐ (x : E) ∂μ, ‖x‖ ≤ b
x : E
hx : ‖x‖ ≤ b
⊢ rexp (HPow.hPow (β := ℕ) ‖x‖ 2) ≤ rexp (HPow.hPow (β := ℕ) b 2)
have h : 0 ≤ ‖x‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : IsFiniteMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
⊢ ∃ (C : ℝ), 0 < C ∧ Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) μ
have pos : ∀ (hμ_zero : μ = 0), ∃ (C : ℝ), 0 < C ∧ Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) μ
Tactic: by_cases hμ_zero : μ = 0
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : IsFiniteMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
pos : ∀ (hμ_zero : μ = 0), ∃ (C : ℝ), 0 < C ∧ Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) μ
⊢ ∃ (C : ℝ), 0 < C ∧ Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) μ
have neg : ∀ (hμ_zero : ¬μ = 0), ∃ (C : ℝ), 0 < C ∧ Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) μ
Tactic: by_cases hμ_zero : μ = 0
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (hypothesis)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : IsFiniteMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
hμ_zero : ¬μ = 0
μ' : Measure E := μ[|Set.univ]
⊢ ∃ (C : ℝ), 0 < C ∧ Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) μ
have hμ'_eq : μ' = HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) μ
Tactic: have hμ'_eq : μ' = (μ .univ)⁻¹ • μ := by simp [μ', cond]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (hypothesis)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : IsFiniteMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
hμ_zero : ¬μ = 0
μ' : Measure E := μ[|Set.univ]
hμ'_eq : μ' = HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) μ
⊢ ∃ (C : ℝ), 0 < C ∧ Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) μ
have hμ' : IsProbabilityMeasure μ'
Tactic: have hμ' : IsProbabilityMeasure μ' := cond_isProbabilityMeasure <| by simp [hμ_zero]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : IsFiniteMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
hμ_zero : ¬μ = 0
μ' : Measure E := μ[|Set.univ]
hμ'_eq : μ' = HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) μ
hμ' : IsProbabilityMeasure μ'
⊢ HSMul.hSMul (β := Measure (E × E))
      (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞)
        (((μ : (a : Set E) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞))
      (Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ)) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞)
        (((μ : (a : Set E) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) •
      μ.prod μ
have rw : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞)
      (((μ : (a : Set E) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) •
    μ.prod μ =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞)
      (((μ : (a : Set E) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) •
    μ.prod μ
Tactic: rw [h_rot]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : IsFiniteMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
hμ_zero : ¬μ = 0
μ' : Measure E := μ[|Set.univ]
hμ'_eq : μ' = HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) μ
hμ' : IsProbabilityMeasure μ'
⊢ Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ'.prod μ') = μ'.prod μ'
have calc : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ'.prod μ') =
  HSMul.hSMul (β := Measure (E × E))
    (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞)
      (((μ : (a : Set E) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞))
    (Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ))
Tactic: calc (μ'.prod μ').map (ContinuousLinearMap.rotation (-(π / 4)))
    _ = ((μ Set.univ)⁻¹ * (μ Set.univ)⁻¹)
        • (μ.prod μ).map (ContinuousLinearMap.rotation (-(π / 4))) := by
      simp [hμ'_eq, Measure.prod_smul_left, Measure.prod_smul_right, smul_smul]
    _ = ((μ Set.univ)⁻¹ * (μ Set.univ)⁻¹) • (μ.prod μ) := by rw [h_rot]
    _ = μ'.prod μ' := by
      simp [hμ'_eq, Measure.prod_smul_left, Measure.prod_smul_right, smul_smul]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : IsFiniteMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
hμ_zero : ¬μ = 0
μ' : Measure E := μ[|Set.univ]
hμ'_eq : μ' = HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) μ
hμ' : IsProbabilityMeasure μ'
calc :
  Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ'.prod μ') =
    HSMul.hSMul (β := Measure (E × E))
      (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞)
        (((μ : (a : Set E) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞))
      (Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ))
⊢ Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ'.prod μ') = μ'.prod μ'
have calc₁ : HSMul.hSMul (β := Measure (E × E))
    (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞)
      (((μ : (a : Set E) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞))
    (Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ)) =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞)
      (((μ : (a : Set E) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) •
    μ.prod μ
Tactic: calc (μ'.prod μ').map (ContinuousLinearMap.rotation (-(π / 4)))
    _ = ((μ Set.univ)⁻¹ * (μ Set.univ)⁻¹)
        • (μ.prod μ).map (ContinuousLinearMap.rotation (-(π / 4))) := by
      simp [hμ'_eq, Measure.prod_smul_left, Measure.prod_smul_right, smul_smul]
    _ = ((μ Set.univ)⁻¹ * (μ Set.univ)⁻¹) • (μ.prod μ) := by rw [h_rot]
    _ = μ'.prod μ' := by
      simp [hμ'_eq, Measure.prod_smul_left, Measure.prod_smul_right, smul_smul]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : IsFiniteMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
hμ_zero : ¬μ = 0
μ' : Measure E := μ[|Set.univ]
hμ'_eq : μ' = HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) μ
hμ' : IsProbabilityMeasure μ'
calc :
  Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ'.prod μ') =
    HSMul.hSMul (β := Measure (E × E))
      (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞)
        (((μ : (a : Set E) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞))
      (Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ))
calc₁ :
  HSMul.hSMul (β := Measure (E × E))
      (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞)
        (((μ : (a : Set E) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞))
      (Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ)) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞)
        (((μ : (a : Set E) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) •
      μ.prod μ
⊢ Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ'.prod μ') = μ'.prod μ'
have calc₂ : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞)
      (((μ : (a : Set E) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) •
    μ.prod μ =
  μ'.prod μ'
Tactic: calc (μ'.prod μ').map (ContinuousLinearMap.rotation (-(π / 4)))
    _ = ((μ Set.univ)⁻¹ * (μ Set.univ)⁻¹)
        • (μ.prod μ).map (ContinuousLinearMap.rotation (-(π / 4))) := by
      simp [hμ'_eq, Measure.prod_smul_left, Measure.prod_smul_right, smul_smul]
    _ = ((μ Set.univ)⁻¹ * (μ Set.univ)⁻¹) • (μ.prod μ) := by rw [h_rot]
    _ = μ'.prod μ' := by
      simp [hμ'_eq, Measure.prod_smul_left, Measure.prod_smul_right, smul_smul]