test module

`Tests.SupportLocalBlocks`

0 named declarations scanned from Tests/SupportLocalBlocks.lean.

Imports

AutoSamplingTheory.TechnicalLemmas.Measure.SupportLocalBlocks

Imported by

No local reverse import.

Placeholder scan

0 declaration(s) flagged

Gate status

Partial

Declarations

This aggregator contains no named declarations.

Complete Lean source

Tests/SupportLocalBlocks.lean — full module with imports and context

Download module (.lean)

import AutoSamplingTheory.TechnicalLemmas.Measure.SupportLocalBlocks

#check AutoSamplingTheory.TechnicalLemmas.Measure.SupportLocalBlocks.restrict_mass_pos_of_mem_support_of_isOpen
#check AutoSamplingTheory.TechnicalLemmas.Measure.SupportLocalBlocks.sum_restrict_le_of_pairwiseDisjoint_open
#check AutoSamplingTheory.TechnicalLemmas.Measure.SupportLocalBlocks.rectangle_restrict_mass_pos
#check AutoSamplingTheory.TechnicalLemmas.Measure.SupportLocalBlocks.exists_positive_local_blocks_of_cycleValue_pos