OAI/Analysis/RieszRectifiability/Kernel/PartitionSecondMoments.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Second moments from partition approximations

Convergence of partition masses and coefficients gives convergence of finite-step L² norms. Vanishing squared approximation errors then transfer this convergence to the second moments of the original functions under varying measures.

  1. theorem OAI.RieszRectifiability.tendsto_of_squared_approximation line 20
  2. theorem OAI.RieszRectifiability.finiteStep_L2_norm_tendsto line 43
  3. theorem OAI.RieszRectifiability.toLp_norm_difference_sq_le line 58
  4. theorem OAI.RieszRectifiability.partition_approximation_second_moments_tendsto line 66