Average the actual signed Gaussian normalization factor

The exact module derives integrability, reflection algebra, law preservation, finite expansion and survivor evaluation internally. The Borel premise is retained from the source even where L1 already supplies the measurability needed by a bounded-multiplier step.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem signed_sqrt_det_integral {n : ℕ} (hn : 3 ≤ n) {κ : ℝ} (hκ : 4 ≤ κ)
    (h : ℝ → ℝ) (hh : Measurable h)
    (hL1 : Integrable (fun O : Matrix.orthogonalGroup (Fin n) ℝ => h ((O : Matrix (Fin n) (Fin n) ℝ) (⟨0, lt_of_lt_of_le (by decide : 0 < 3) hn⟩ : Fin n) (⟨0, lt_of_lt_of_le (by decide : 0 < 3) hn⟩ : Fin n))) (orthogonalHaar n)) :
    (∫ O : Matrix.orthogonalGroup (Fin n) ℝ,
      (O : Matrix (Fin n) (Fin n) ℝ).det * Real.sqrt (singleBlockPrecision κ O).det *
        h ((O : Matrix (Fin n) (Fin n) ℝ) (⟨0, lt_of_lt_of_le (by decide : 0 < 3) hn⟩ : Fin n) (⟨0, lt_of_lt_of_le (by decide : 0 < 3) hn⟩ : Fin n)) ∂orthogonalHaar n) =
      ((-1 : ℝ) ^ (n - 1) * (Real.sqrt κ - 1) ^ (n - 1) / (2 : ℝ) ^ n) *
        (∫ O : Matrix.orthogonalGroup (Fin n) ℝ,
          ((Real.sqrt κ + 1) * ((O : Matrix (Fin n) (Fin n) ℝ) (⟨0, lt_of_lt_of_le (by decide : 0 < 3) hn⟩ : Fin n) (⟨0, lt_of_lt_of_le (by decide : 0 < 3) hn⟩ : Fin n)) - (Real.sqrt κ - 1)) *
            h ((O : Matrix (Fin n) (Fin n) ℝ) (⟨0, lt_of_lt_of_le (by decide : 0 < 3) hn⟩ : Fin n) (⟨0, lt_of_lt_of_le (by decide : 0 < 3) hn⟩ : Fin n)) ∂orthogonalHaar n) := by
  classical
  let j0 : Fin n := ⟨0, lt_of_lt_of_le (by decide : 0 < 3) hn⟩
  let U (O : Matrix.orthogonalGroup (Fin n) ℝ) : ℝ :=
    (O : Matrix (Fin n) (Fin n) ℝ) j0 j0
  let g : Matrix.orthogonalGroup (Fin n) ℝ → ℝ := fun O => h (U O)
  let a := Real.sqrt κ + 1
  let b := Real.sqrt κ - 1
  change (∫ O : Matrix.orthogonalGroup (Fin n) ℝ,
      (O : Matrix (Fin n) (Fin n) ℝ).det * Real.sqrt (singleBlockPrecision κ O).det *
        g O ∂orthogonalHaar n) =
    ((-1 : ℝ) ^ (n - 1) * b ^ (n - 1) / (2 : ℝ) ^ n) *
      (∫ O : Matrix.orthogonalGroup (Fin n) ℝ, (a * U O - b) * g O ∂orthogonalHaar n)
  have hnorm : ∀ O : Matrix.orthogonalGroup (Fin n) ℝ,
      (O : Matrix (Fin n) (Fin n) ℝ).det * Real.sqrt (singleBlockPrecision κ O).det =
        (1 / (2 : ℝ) ^ n) *
          (a • (O : Matrix (Fin n) (Fin n) ℝ) + (-b) • (1 : Matrix (Fin n) (Fin n) ℝ)).det := by
    intro O
    simpa only [a, b, neg_smul, sub_eq_add_neg] using singleBlockPrecision_signed_sqrt_det hn hκ O
  have hstep : (∫ O : Matrix.orthogonalGroup (Fin n) ℝ,
      (O : Matrix (Fin n) (Fin n) ℝ).det * Real.sqrt (singleBlockPrecision κ O).det *
        g O ∂orthogonalHaar n) =
      (1 / (2 : ℝ) ^ n) * (∫ O : Matrix.orthogonalGroup (Fin n) ℝ,
        (a • (O : Matrix (Fin n) (Fin n) ℝ) + (-b) • (1 : Matrix (Fin n) (Fin n) ℝ)).det *
          g O ∂orthogonalHaar n) := by
    calc
      _ = ∫ O : Matrix.orthogonalGroup (Fin n) ℝ, (1 / (2 : ℝ) ^ n) *
          ((a • (O : Matrix (Fin n) (Fin n) ℝ) + (-b) •
            (1 : Matrix (Fin n) (Fin n) ℝ)).det * g O) ∂orthogonalHaar n := by
        apply integral_congr_ae
        exact Filter.Eventually.of_forall fun O => by
          dsimp only
          rw [hnorm O]
          ring
      _ = _ := integral_const_mul _ _
  have havg := affine_det_weighted_average hn a (-b) h hh hL1
  change (∫ O : Matrix.orthogonalGroup (Fin n) ℝ,
      (a • (O : Matrix (Fin n) (Fin n) ℝ) + (-b) • (1 : Matrix (Fin n) (Fin n) ℝ)).det *
        g O ∂orthogonalHaar n) =
      (-b) ^ n * (∫ O, g O ∂orthogonalHaar n) +
        a * (-b) ^ (n - 1) * (∫ O, U O * g O ∂orthogonalHaar n) at havg
  have hUc : Continuous U := by
    dsimp only [U]
    exact (continuous_apply j0).comp ((continuous_apply j0).comp continuous_subtype_val)
  have hU : Integrable (fun O => U O * g O) (orthogonalHaar n) :=
    hL1.bdd_mul hUc.measurable.aestronglyMeasurable
      (show ∀ᵐ O : Matrix.orthogonalGroup (Fin n) ℝ ∂orthogonalHaar n, ‖U O‖ ≤ (1 : ℝ) from
        Filter.Eventually.of_forall fun O => entry_norm_bound_of_unitary O.property j0 j0)
  have hlin : (∫ O : Matrix.orthogonalGroup (Fin n) ℝ, (a * U O - b) * g O ∂orthogonalHaar n) =
      a * (∫ O, U O * g O ∂orthogonalHaar n) - b * (∫ O, g O ∂orthogonalHaar n) := by
    calc
      _ = ∫ O : Matrix.orthogonalGroup (Fin n) ℝ,
          a * (U O * g O) - b * g O ∂orthogonalHaar n := by
        apply integral_congr_ae
        exact Filter.Eventually.of_forall fun O => by ring
      _ = _ := by
        rw [integral_sub (hU.const_mul a) (hL1.const_mul b), integral_const_mul, integral_const_mul]
  rw [hstep, havg, hlin]
  have hn' : n - 1 + 1 = n := by omega
  have hp : (-b) ^ n = (-b) ^ (n - 1) * (-b) := by
    conv_lhs => rw [← hn', pow_succ]
  rw [hp]
  rw [neg_pow b (n - 1)]
  simp only [div_eq_mul_inv]
  ring


end AutoSamplingTheory.ExampleCases.GaussianComplexity.DeterminantCancellation

Exact module and namespace context